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

On Fri, 4 Jul 2014 09:24:40 +0200, Gautier DI FOLCO 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.