[Haskell-cafe] Type-level Nat to Integer

[Gautier DI FOLCO]

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).
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140704/f62a7a9c/attachment.html>