TypeNats trial on new ghc branch 7.8
Iavor Diatchki
iavor.diatchki at gmail.com
Sat Feb 1 21:38:46 UTC 2014
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>
More information about the ghc-devs
mailing list