[Haskell-cafe] Type-level Nat to Integer

[Andras Slemmer]

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


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