TypeLits

[Carter Schonwald]

hey Iavor,
I just tried out today's head on a slightly more interesting example, and i
hit the limits of the type nat solver,

http://ghc.haskell.org/trac/ghc/ticket/8422#comment:1

it seems like something where the solver *should* work


On Mon, Oct 7, 2013 at 1:35 AM, Iavor Diatchki <iavor.diatchki at gmail.com>wrote:

> 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/20131008/1814353c/attachment.html>