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

4 Jul 2014


      2014-07-04 10:00 GMT+02:00 Niklas Haas :
...
On Fri, 4 Jul 2014 09:24:40 +0200, Gautier DI FOLCO <
gautier.difolco@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.