TypeNats trial on new ghc branch 7.8

[Iavor Diatchki]

Hi,

yep that's exactly the case---the current solver can only do things like "2
+ 3 ~ 5".   The interesting new solver, which knows about linear
arithmetic, is currently on branch "decision-procedure"  but that's quite
out of date.  I am waiting for 7.8 to get out the door, and than I plan to
restart working on this, to get it updated and on the master branch,
hopefully to be part of the following GHC release.

-Iavor


On Sat, Feb 1, 2014 at 8:03 AM, Carter Schonwald <carter.schonwald at gmail.com
> wrote:

> Hey Gabriel,
> As far as I could determine, there is no solver powers in 7.8
> the "solver" can simply just check that  (2 + 3 )~5 and other simple
> "compute to get equality" situations
>
>
> On Sat, Feb 1, 2014 at 10:52 AM, Christiaan Baaij <
> christiaan.baaij at gmail.com> wrote:
>
>> The "simplified" solver, as in
>> https://github.com/ghc/ghc/tree/type-nats-simple, has been integrated as
>> far as I know.
>> I've been experimenting with my own solver:
>> https://gist.github.com/christiaanb/8396614
>> Here are some examples of the stuff that works with my solver:
>> https://github.com/christiaanb/clash-prelude/blob/newnats/src/CLaSH/Sized/Vector.hs
>>
>>
>> On Sat, Feb 1, 2014 at 4:23 PM, Gabriel Riba <griba2001 at gmail.com> wrote:
>>
>>> I know that the TypeNats solver may not have been merged with 7.8 branch
>>>
>>> but the compiler error looks so simple:
>>>
>>> Couldn't match type ‛(n + m) - 1’ with ‛(n - 1) + m’
>>>
>>>     ---------------------------------
>>>     {-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeOperators,
>>> PolyKinds,
>>> ExistentialQuantification #-}
>>>
>>>     import GHC.TypeLits
>>>
>>>     data Vect :: Nat -> * -> * where
>>>       Nil ::  Vect 0 a
>>>       Cons :: a -> Vect (n-1) a -> Vect n a
>>>
>>>     data MyProxy (n::Nat) = forall a. MyProxy (Vect n a)
>>>
>>>     toProxy :: Vect (n::Nat) a -> MyProxy n
>>>     toProxy v = MyProxy v
>>>
>>>     len :: KnownNat n => Vect (n::Nat) a -> Integer
>>>     len v = (natVal . toProxy) v                         -- Ok
>>>
>>>     append :: Vect n a -> Vect m a -> Vect (n+m) a
>>>     append Nil ys = ys
>>>     append (Cons x xs) ys = Cons x (append xs ys)  -- compiler error
>>>
>>>
>>>     main = do
>>>       print $ len Nil                          -- Ok
>>>       print $ len (Cons (1::Int) Nil)          -- Ok
>>>     ------------------------------------------------------
>>>
>>>
>>> Error on "append  (Cons x xs) ys = ..."
>>>
>>>     Couldn't match type ‛(n + m) - 1’ with ‛(n - 1) + m’
>>>     Expected type: Vect ((n + m) - 1) a
>>>       Actual type: Vect ((n - 1) + m) a
>>>
>>>
>>>
>>> _______________________________________________
>>> ghc-devs mailing list
>>> ghc-devs at haskell.org
>>> http://www.haskell.org/mailman/listinfo/ghc-devs
>>>
>>
>>
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://www.haskell.org/mailman/listinfo/ghc-devs
>>
>>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140201/737ce4a6/attachment-0001.html>