Iterating over SList Nat to produce product of elements

Learn
#1

Hi Haskellers!

I am trying to understand how to iterate over a singleton list of nats to produce the product of their integer value to use at runtime.

I have tried the following

listToInt :: forall (ns :: [Nat]). SList ns -> Integer
listToInt SNil = 1
listToInt (SCons x xs) = natVal x * listToInt xs

but I get the following error:

    • Could not deduce (KnownNat n1) arising from a use of ‘natVal’
      from the context: ns ~ (n1 : n2)
        bound by a pattern with constructor:
                   SCons :: forall a0 (n1 :: a0) (n2 :: [a0]).
                            singletons-2.6:Data.Singletons.Internal.Sing n1
                            -> singletons-2.6:Data.Singletons.Internal.Sing n2
                            -> SList (n1 : n2),
                 in an equation for ‘listToInt’
        at src/Frechet/Eval.hs:18:12-21
      Possible fix:
        add (KnownNat n1) to the context of the data constructor ‘SCons’
    • In the first argument of ‘(*)’, namely ‘natVal x’
      In the expression: natVal x * listToInt xs
      In an equation for ‘listToInt’:
          listToInt (SCons x xs) = natVal x * listToInt xs
   |
18 | listToInt (SCons x xs) = natVal x * listToInt xs
   |                          ^^^^^^^^

Any idea how to do this?

Thanks!
Ahmad Salim

#2

Oh, I needed the withKnownNat function! :smile:

1 Like