[Haskell-cafe] Type-level Nat to Integer

[Gautier DI FOLCO]

2014-07-04 10:00 GMT+02:00 Niklas Haas <haskell at nand.wakku.to>:

> On Fri, 4 Jul 2014 09:24:40 +0200, Gautier DI FOLCO <
> gautier.difolco at gmail.com> wrote:
> > data Vector :: Nat -> * -> * where
> >     Nil ::                     Vector Z a
> >     El  :: a -> Vector n a  -> Vector (S n) a
> >
> > lengthV :: NatToInt l => Vector l a -> Int
> > lengthV _ = natToInt (Proxy :: Proxy l)
>
> You can do this without ScopedTypeVariables using a small helper
> function:
>
> lengthV :: NatToInt l => Vector l a -> Int
> lengthV = natToInt . (const Proxy :: Vector l' a' -> Proxy l')
>
> Note that this function is again polymorphic, hence no
> ScopedTypeVariables required.
>

Interesting, thanks.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140704/10dc212d/attachment.html>