[Haskell-cafe] Type-level Nat to Integer

[Christiaan Baaij]

On Jul 4, 2014, at 9:39 AM, Gautier DI FOLCO <gautier.difolco at gmail.com> wrote:

> 2014-07-04 9:30 GMT+02:00 Tikhon Jelvis <tikhon at jelv.is>:
> 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