[Haskell-cafe] Type-level Nat to Integer

[Gautier DI FOLCO]

2014-07-04 8:57 GMT+02:00 Gautier DI FOLCO <gautier.difolco at gmail.com>:

> 2014-07-04 0:04 GMT+02:00 Andras Slemmer <0slemi0 at gmail.com>:
>
> Also, check out the singletons library, it handles type promotion/demotion
>> pretty well. In particular the
>> https://hackage.haskell.org/package/singletons-1.0/docs/Data-Singletons.html#t:SingKind
>> typeclass handles demotion with fromSing
>>
>
> It's a little bit complicated for me at the time, but I'll have a look.
>
>
>>
>>
>> On 3 July 2014 14:39, Andres Löh <andres at well-typed.com> wrote:
>>
>>> Hi.
>>>
>>> In
>>>
>>> > class NatToInt n where
>>> >    natToInt :: n -> Int
>>>
>>> the class parameter is of kind "Nat", but a function argument has to
>>> be of kind "*". However, you only want the "n" argument in order to
>>> "guide" the instance resolution mechanism. For this, you can use a
>>> "Proxy". A Proxy is a datatype that is parameterized by an arbitrary
>>> argument (of arbitrary kind), but has only one value, also called
>>> "Proxy", so it's perfect for an argument that has no computational
>>> meaning and is just there to make the type checker happy:
>>>
>>> > {-# LANGUAGE DataKinds, KindSignatures, GADTs, PolyKinds,
>>> ScopedTypeVariables #-}
>>> >
>>> > import Data.Proxy
>>> >
>>> > data Nat = Z | S Nat
>>> >
>>> > class NatToInt n where
>>> >     natToInt :: Proxy n -> Int
>>> >
>>> > instance NatToInt Z where
>>> >     natToInt _ = 0
>>> >
>>> > instance NatToInt n => NatToInt (S n) where
>>> >     natToInt _ = 1 + natToInt (Proxy :: Proxy n)
>>>
>>> Cheers,
>>>   Andres
>>>
>>> --
>>> Andres Löh, Haskell Consultant
>>> Well-Typed LLP, http://www.well-typed.com
>>>
>>> Registered in England & Wales, OC335890
>>> 250 Ice Wharf, 17 New Wharf Road, London N1 9RF, England
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>
>>
>>
> Thanks (I finally understand the usefulness of Proxy).
>

I have an additional question: How can I "extract" a type variable?
I want to do something like this:

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)


Thanks in advance for your answers.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140704/774053aa/attachment.html>