[Haskell-cafe] Type-level Nat to Integer

[Niklas Haas]

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.