Re: [Haskell-cafe] Type-level Nat to Integer

2014-07-04 9:51 GMT+02:00 Christiaan Baaij :

On Jul 4, 2014, at 9:39 AM, Gautier DI FOLCO wrote:

...

2014-07-04 9:30 GMT+02:00 Tikhon Jelvis : You probably want the ScopedTypeVariables extension. You'll also have to qualify the relevant variable with an explicit forall:

forall l. NatToInt l => ...

Then you can use l in your expression and it will be in scope.

Interesting, what it's the semantic which force me to add an explicit for all?

In the case you want to be _less_ general. That is, in you original code:

...

lengthV :: NatToInt l => Vector l a -> Int lengthV _ = natToInt (Proxy :: Proxy l)

the two 'l' variables are not necessarily the same, that is, the compiler sees your code as:

...

lengthV :: NatToInt l => Vector l a -> Int lengthV _ = natToInt (Proxy :: Proxy l1)

Notice that there are now two type variables, 'l' and 'l1', which is a more general function. In you case however, you want the 'l' in the where clause to be the same as the 'l' in your top-level type signature. So then you write:

...

lengthV :: forall l . NatToInt l => Vector l a -> Int lengthV _ = natToInt (Proxy :: Proxy l)

Which is less general, but exactly what you want.

-- Christiaan

ok, so forall add some constraints in this case. Thanks.