TypeLits

[Carter Schonwald]

gotcha

what are the   technical obstacles to getting solver for at least
Presburger Arithmetic in?

 I'd be willing to even do the footwork if there was any shadow of a chance
of geting that into 7.8 as a *bugfix*
(or failing that, helping kick it along post 7.8, but i've enough other
contribs planned post 7.8 release)

cheers
-Carter


On Tue, Oct 8, 2013 at 7:49 PM, Iavor Diatchki <iavor.diatchki at gmail.com>wrote:

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