[Haskell-cafe] Type-level Nat to Integer

[Tikhon Jelvis]

You probably want the ScopedTypeVariables extension. You'll also have to
qualify the relevant variable with an explicit forall:

    forall l. NatToInt l => ...

Then you can use l in your expression and it will be in scope.
On Jul 4, 2014 12:25 AM, "Gautier DI FOLCO" <gautier.difolco at gmail.com>
wrote:

> 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.
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140704/1d540ca2/attachment.html>