TypeLits

[Iavor Diatchki]

Hi,


On Sun, Oct 6, 2013 at 4:36 PM, Carter Schonwald <carter.schonwald at gmail.com
> wrote:

> hrmm, Why don't we have a proper bijection?
>
> lets assume we have ToPeano and a corresponding ToNat, as above,
>
> couldn't we have something like
>
> asPeano :: (b~ ToPeano a, a ~ ToNat b)=> Proxy a -> Proxy b
>
> or a suitable type level representaion thereof?
>
>  I think it should be quite easy to define such a function, but I am
afraid I don't fully understand how to use it...



> or are you saying that in 7.8, i should be able to just efficiently work
> directly on the nat rep
>
> and have
>
> class Cl (n::Nat) where
>
> instance CL 0 where
>
> instance Cl n => Cl (n+1)
>
> and essentially get peano for free?
>
>
>>>>>>
I am not sure if this would help with your specific task, but things like
this work:


{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}
{-# LANGUAGE FlexibleInstances, UndecidableInstances, OverlappingInstances
#-}
import GHC.TypeLits
import Data.Proxy

class C (n :: Nat) where
  txt :: Proxy n -> String

instance C 0 where
  txt _ = "0"

instance C (n - 1) => C n where
  txt x = "1 + " ++ txt (prev x)

prev :: Proxy x -> Proxy (x - 1)
prev _ = Proxy

example = txt (Proxy :: Proxy 3)

*Main> example
"1 + 1 + 1 + 0"

-Iavor
PS: All of this is committed in HEAD, please try it out and let me know if
we need to do any last minute changes before the upcoming release.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20131006/55fee155/attachment.html>