TypeLits

[Iavor Diatchki]

Hi,

yeah, I know :-)  The current solver can only evaluate concrete things, for
example it knows that 5 + 3 ~ 8,
but it can't do any abstract reasoning (i.e., when there are variables
around).  So things like GADTs pretty much don't work at the moment.

-Iavor


On Tue, Oct 8, 2013 at 2:08 PM, Carter Schonwald <carter.schonwald at gmail.com
> wrote:

> 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/a70e6329/attachment.html>