TypeLits

Carter Schonwald carter.schonwald
Wed Oct 9 01:01:22 UTC 2013


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>




More information about the Libraries mailing list