[Haskell-cafe] Type-level Nat to Integer

[Gautier DI FOLCO]

2014-07-04 9:51 GMT+02:00 Christiaan Baaij <christiaan.baaij at gmail.com>:

>
> 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
>
>
ok, so forall add some constraints in this case.

Thanks.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140704/668e5a6d/attachment.html>