TypeNats trial on new ghc branch 7.8

Gabriel Riba

1 Feb 2014 1 Feb '14

3:23 p.m.

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

Show replies by date

Christiaan Baaij

1 Feb 1 Feb

3:52 p.m.

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/Ve... On Sat, Feb 1, 2014 at 4:23 PM, Gabriel Riba 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@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

Carter Schonwald

4:03 p.m.

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@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/Ve...

On Sat, Feb 1, 2014 at 4:23 PM, Gabriel Riba 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@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

Iavor Diatchki

9:38 p.m.

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

...

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@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/Ve...

On Sat, Feb 1, 2014 at 4:23 PM, Gabriel Riba 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@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

4175

Age (days ago)

4175

Last active (days ago)

List overview

Download

3 comments

4 participants

participants (4)

Carter Schonwald
Christiaan Baaij
Gabriel Riba
Iavor Diatchki