its a special Thing that just uses Integer internally, but because it doenst provide a PEANO api, we can't do computations on it :'( On Sun, Mar 16, 2014 at 10:37 AM, Henning Thielemann < lemming@henning-thielemann.de> wrote:

Am 16.03.2014 14:35, schrieb Carter Schonwald:

You can't with type lits. The solver can only decide concrete values :"""(

...

I hoped that with type-level natural numbers all my dreams would become true. :-)

I'd be also happy if I could manually provide the proof for 1<=n+1 and more complicated statements like n+n=2*n and n>0 && m>0 => n*m>0.

You'll have to use a concrete peano Nats type instead.

...

That is, I may as well stay with the existing type-level number packages?

I've been toying with the idea that the type lits syntax should be just

...

that, a type level analogue of from integer that you can give to user land types, but I'm not going to suggest that till 7.8 is fully released.

Seems reasonable. By the way, is the GHC Nat kind defined by data promotion or is it a special kind with an efficient internal representation?

respectfully, The current typeLits story for nats is kinda a fuster cluck to put it politely . We have type lits but we cant use them (well, we can't compute on them, which is the same thing). For the past 2 years, every ghc release cycle, I first discover, then have to communicate to everyone else "you can't compute on type lits". Heres what I'd like to happen for 7.10, and i'm happy to help / pester this along 1) Typelits as it currently exists in GHC actually conflates "syntactic support" for Nats with having primacy as the "nat" type for ghc. I think we should seriously consider moving in a direction akin to how Agda provides syntactic/ computational support for efficient / 2) the current typelits supplied Nat is kinda crippled because we can't do userland reasoning / compute on it, I consider this a bug! I'm still waiting (2 years later) for a solver we can actually include in ghc or even a user land solver! i think (1) and some part of (2) should happen for 7.10. What design work / subtleties might block it? On Sun, Mar 16, 2014 at 11:06 AM, Christiaan Baaij < christiaan.baaij@gmail.com> wrote:

Iavor is working on a branch that allows the constraint solver to call an external solver: https://github.com/ghc/ghc/tree/decision-procedure Currently, it: a) only supports CVC4 (an SMT solver), and b) is slightly out of of line with HEAD. I think the above branch will be able to solve things like: 1 <= n + 1 ~ True

I myself worked on a patch that can only work with equalities: https://gist.github.com/christiaanb/8396614 It allows you to solve both more and less constraints than Iavor's CVC4 approach: More: It can deal with non-constant multiplications, and also with exponentials Less: It cannot deal with inequalities

On Sun, Mar 16, 2014 at 1:44 PM, Henning Thielemann < lemming@henning-thielemann.de> wrote:

...

Am 16.03.2014 09:40, schrieb Christiaan Baaij:

To answer the second question (under the assumption that you want

...

phantom-type style Vectors and not GADT-style):

Now I like to define non-empty vectors. The phantom parameter for the length shall refer to the actual vector length, not to length-1, for consistency between possibly empty and non-empty vectors.

I have modified your code as follows:

{-# LANGUAGE Rank2Types #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-} module PositiveNat where

import Data.Proxy (Proxy(Proxy)) import GHC.TypeLits (Nat, SomeNat(SomeNat), KnownNat, someNatVal, natVal, type (<=), type (+))

data Vector (n :: Nat) a = Vector a [a]

withVector :: forall a b. a -> [a] -> (forall n . (KnownNat n, 1<=n) => Vector n a -> b) -> b withVector x xs f = case someNatVal $ toInteger $ length xs of Nothing -> error "static/dynamic mismatch" Just (SomeNat (_ :: Proxy m)) -> f (Vector x xs :: Vector (m+1) a)

vecLen :: forall n . KnownNat n => Vector n Integer -> Integer vecLen _ = natVal (Proxy :: Proxy n)

-- > withVector vecLen [1,2,3,4] -- 4

GHC-7.8 complains with:

PositiveNat.hs:23:40: Could not deduce ((1 GHC.TypeLits.<=? (n + 1)) ~ 'True) from the context (KnownNat n) bound by a pattern with constructor SomeNat :: forall (n :: Nat). KnownNat n => Proxy n -> SomeNat, in a case alternative at PositiveNat.hs:23:13-34 In the expression: f (Vector x xs :: Vector (m + 1) a) In a case alternative: Just (SomeNat (_ :: Proxy m)) -> f (Vector x xs :: Vector (m + 1) a) In the expression: case someNatVal $ toInteger $ length xs of { Nothing -> error "static/dynamic mismatch" Just (SomeNat (_ :: Proxy m)) -> f (Vector x xs :: Vector (m + 1) a) }

How can I convince GHC that n+1 is always at least 1?

When I remove the (1<=n) constraint, I still get:

PositiveNat.hs:23:40: Could not deduce (KnownNat (n + 1)) arising from a use of ‘f’ from the context (KnownNat n) bound by a pattern with constructor SomeNat :: forall (n :: Nat). KnownNat n => Proxy n -> SomeNat, in a case alternative at PositiveNat.hs:23:13-34 In the expression: f (Vector x xs :: Vector (m + 1) a) In a case alternative: Just (SomeNat (_ :: Proxy m)) -> f (Vector x xs :: Vector (m + 1) a) In the expression: case someNatVal (toInteger (length xs)) of { Nothing -> error "static/dynamic mismatch" Just (SomeNat (_ :: Proxy m)) -> f (Vector x xs :: Vector (m + 1) a) }

That is, I also have to convince GHC, that if (KnownNat n) then (n+1) is also KnownNat. How to do that?

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

So much to respond to! First, a little relevant context: Iavor Diatchki is the primary implementor of the type-lits stuff; I am not. But, he and I are playing in the same playground, so to speak, so we confer a fair amount and I may have some helpful perspective on all of this. Henning asks:

How can I convince GHC that n+1 is always at least 1?

You can ramrod facts like this down GHC's throat when necessary. For example, the following works:

foo :: (1 <= n + 1) => Proxy n -> () foo _ = ()

lt :: Proxy n -> (1 <=? n + 1) :~: True lt _ = unsafeCoerce Refl

bar :: forall (n :: Nat). Proxy n -> () bar p = gcastWith (lt p) (foo p)

In case you're unfamiliar with them, here are some helpful definitions from Data.Type.Equality, used above:

data a :~: b where Refl :: a :~: a gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r

Also helpful when doing things like this is this definition, from Edward Kmett's `constraints` package:

data Dict c where Dict :: c => Dict c

An `unsafeCoerce Dict` can be used to satisfy any arbitrary constraint. Of course, it is often possible to use an inductive proof (er, recursive function) to produce Refl or Dict without resorting to unsafeCoerce. But, as the TypeLits Nat isn't inductive, we're forced to use drastic measures here. Carter says:

I've been toying with the idea that the type lits syntax should be just that, a type level analogue of from integer that you can give to user land types, but I'm not going to suggest that till 7.8 is fully released.

I like this idea. Christiaan says:

Iavor is working on a branch that allows the constraint solver to call an external solver: https://github.com/ghc/ghc/tree/decision-procedure

Yes, though I don't know how active this branch is currently. There are whispers afoot of going in the direction of strapping an SMT solver into GHC, though much work remains to be done before this happens. My sense is that an SMT solver will be necessary before TypeLits really becomes fluently useful. I'm confident this will happen eventually, but it may be over a year out, still. It's even possible that I will be the one to do it, but it's not on my short-to-do-list. Christiaan says:

I myself worked on a patch that can only work with equalities: https://gist.github.com/christiaanb/8396614

Cool! Have you conferred with Iavor about this? Carter says:

The current typeLits story for nats is kinda a fuster cluck to put it politely . We have type lits but we cant use them (well, we can't compute on them, which is the same thing).

I disagree on both counts here. TypeLits is a work in progress, as are many parts of GHC. That's one of the beautiful things about Haskell/GHC! Is there more progress to be made? Absolutely. But, without the work that's already been done, I'm not sure we would be as convinced as we are (still not 100%, to be sure, but getting there) that we need an SMT solver. We have to build on previous work, and to do that, we have to write potentially incomplete features. And, I've been able to use TypeLits most of the way toward implementing my `units` library (a way of type-checking with respect to units-of-measure). The only feature that they couldn't support was automatic unit conversions. Carter says:

I'm still waiting (2 years later) for a solver we can actually include in ghc or even a user land solver!

I've done some thinking about user-land solvers and am quite interested in seeing it done. My chief thrust right now is about dependent types in Haskell, not this, but Iavor's "decision-procedure" branch lays a lot of the groundwork down for integrating perhaps multiple solvers in with GHC. Henning says:

A minimal invasive solution would be to provide a kind for unary type level numbers and type functions that convert between Unary and Nat.

This definition is quite straightforward and works beautifully:

data Nat1 = Zero | Succ Nat1 type family U n where U 0 = Zero U n = Succ (U (n-1))

Iavor made sure that subtraction worked specifically in this case because it was so useful. I hope this is helpful! Richard On Mar 16, 2014, at 4:52 PM, Henning Thielemann wrote:

Am 16.03.2014 20:02, schrieb Carter Schonwald:

...

respectfully, The current typeLits story for nats is kinda a fuster cluck to put it politely . We have type lits but we cant use them (well, we can't compute on them, which is the same thing).

For the past 2 years, every ghc release cycle, I first discover, then have to communicate to everyone else "you can't compute on type lits".

A minimal invasive solution would be to provide a kind for unary type level numbers and type functions that convert between Unary and Nat.

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

I had to enable undecidable instances, but I'm very very very happy with the U trick, no TH or other things needed. Thanks :) On Mon, Mar 17, 2014 at 2:52 PM, Carter Schonwald < carter.schonwald@gmail.com> wrote:

(aside, pardon my earlier tone, been a bit overloaded the past few weeks, that crossed over to the list)

OOO that works? I guess that gives a decent way of using TypeLits as a concrete input syntax for Peano numbers. Thanks for pointing that out

I think i'm gonna go drop 7.6 support on some code i'm working on if this works :)

On Mon, Mar 17, 2014 at 2:05 PM, Richard Eisenberg wrote:

...

So much to respond to!

First, a little relevant context: Iavor Diatchki is the primary implementor of the type-lits stuff; I am not. But, he and I are playing in the same playground, so to speak, so we confer a fair amount and I may have some helpful perspective on all of this.

Henning asks:

...

How can I convince GHC that n+1 is always at least 1?

You can ramrod facts like this down GHC's throat when necessary. For example, the following works:

...

foo :: (1 <= n + 1) => Proxy n -> () foo _ = ()

lt :: Proxy n -> (1 <=? n + 1) :~: True lt _ = unsafeCoerce Refl

bar :: forall (n :: Nat). Proxy n -> () bar p = gcastWith (lt p) (foo p)

In case you're unfamiliar with them, here are some helpful definitions from Data.Type.Equality, used above:

...

data a :~: b where Refl :: a :~: a gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r

Also helpful when doing things like this is this definition, from Edward Kmett's `constraints` package:

...

data Dict c where Dict :: c => Dict c

An `unsafeCoerce Dict` can be used to satisfy any arbitrary constraint.

Of course, it is often possible to use an inductive proof (er, recursive function) to produce Refl or Dict without resorting to unsafeCoerce. But, as the TypeLits Nat isn't inductive, we're forced to use drastic measures here.

...

I've been toying with the idea that the type lits syntax should be just

Carter says: that, a type level analogue of from integer that you can give to user land types, but I'm not going to suggest that till 7.8 is fully released.

I like this idea.

Christiaan says:

...

Iavor is working on a branch that allows the constraint solver to call an external solver: https://github.com/ghc/ghc/tree/decision-procedure

Yes, though I don't know how active this branch is currently. There are whispers afoot of going in the direction of strapping an SMT solver into GHC, though much work remains to be done before this happens. My sense is that an SMT solver will be necessary before TypeLits really becomes fluently useful. I'm confident this will happen eventually, but it may be over a year out, still. It's even possible that I will be the one to do it, but it's not on my short-to-do-list.

Christiaan says:

...

I myself worked on a patch that can only work with equalities: https://gist.github.com/christiaanb/8396614

Cool! Have you conferred with Iavor about this?

...

The current typeLits story for nats is kinda a fuster cluck to put it

Carter says: politely . We have type lits but we cant use them (well, we can't compute on them, which is the same thing).

I disagree on both counts here. TypeLits is a work in progress, as are many parts of GHC. That's one of the beautiful things about Haskell/GHC! Is there more progress to be made? Absolutely. But, without the work that's already been done, I'm not sure we would be as convinced as we are (still not 100%, to be sure, but getting there) that we need an SMT solver. We have to build on previous work, and to do that, we have to write potentially incomplete features. And, I've been able to use TypeLits most of the way toward implementing my `units` library (a way of type-checking with respect to units-of-measure). The only feature that they couldn't support was automatic unit conversions.

Carter says:

...

I'm still waiting (2 years later) for a solver we can actually include in ghc or even a user land solver!

I've done some thinking about user-land solvers and am quite interested in seeing it done. My chief thrust right now is about dependent types in Haskell, not this, but Iavor's "decision-procedure" branch lays a lot of the groundwork down for integrating perhaps multiple solvers in with GHC.

Henning says:

...

A minimal invasive solution would be to provide a kind for unary type level numbers and type functions that convert between Unary and Nat.

This definition is quite straightforward and works beautifully:

...

data Nat1 = Zero | Succ Nat1 type family U n where U 0 = Zero U n = Succ (U (n-1))

Iavor made sure that subtraction worked specifically in this case because it was so useful.

I hope this is helpful! Richard

On Mar 16, 2014, at 4:52 PM, Henning Thielemann < lemming@henning-thielemann.de> wrote:

...

Am 16.03.2014 20:02, schrieb Carter Schonwald:

...

respectfully, The current typeLits story for nats is kinda a fuster cluck to put it politely . We have type lits but we cant use them (well, we can't compute on them, which is the same thing).

For the past 2 years, every ghc release cycle, I first discover, then have to communicate to everyone else "you can't compute on type lits".

A minimal invasive solution would be to provide a kind for unary type level numbers and type functions that convert between Unary and Nat.

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Would it be correct to think of closed type families as being more like a closed, ordered collection of unification queries against the constraint solver, that happens to act like pattern matching? Does that mean that one possible but potentially ill advised generalization be some sort of way to add pattern guards? I imagine it'd kinda work like instance heads for type classes. I'm not suggesting this mind you, merely thing to understand how to think about the crazy amount of power :) that said, for fake 7.6 support i'm going to have to via CPP export the following opentype family :) type family U (n:: LitNat) :: Nat -- can't induct, hence crippled type instance U n = Z On Tue, Mar 18, 2014 at 9:33 AM, Richard Eisenberg wrote:

Yes, I suppose you would need UndecidableInstances. There's no way for GHC's (already rather weak) termination checker to know that by saying (n-1) a bunch, you're bound to reach 0.

I'm glad it's working for you. When I discovered this application for closed type families, I was rather pleased, myself!

Richard

On Mar 17, 2014, at 4:01 PM, Carter Schonwald wrote:

I had to enable undecidable instances, but I'm very very very happy with the U trick, no TH or other things needed. Thanks :)

On Mon, Mar 17, 2014 at 2:52 PM, Carter Schonwald < carter.schonwald@gmail.com> wrote:

...

(aside, pardon my earlier tone, been a bit overloaded the past few weeks, that crossed over to the list)

OOO that works? I guess that gives a decent way of using TypeLits as a concrete input syntax for Peano numbers. Thanks for pointing that out

I think i'm gonna go drop 7.6 support on some code i'm working on if this works :)

On Mon, Mar 17, 2014 at 2:05 PM, Richard Eisenberg wrote:

...

So much to respond to!

First, a little relevant context: Iavor Diatchki is the primary implementor of the type-lits stuff; I am not. But, he and I are playing in the same playground, so to speak, so we confer a fair amount and I may have some helpful perspective on all of this.

Henning asks:

...

How can I convince GHC that n+1 is always at least 1?

You can ramrod facts like this down GHC's throat when necessary. For example, the following works:

...

foo :: (1 <= n + 1) => Proxy n -> () foo _ = ()

lt :: Proxy n -> (1 <=? n + 1) :~: True lt _ = unsafeCoerce Refl

bar :: forall (n :: Nat). Proxy n -> () bar p = gcastWith (lt p) (foo p)

In case you're unfamiliar with them, here are some helpful definitions from Data.Type.Equality, used above:

...

data a :~: b where Refl :: a :~: a gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r

Also helpful when doing things like this is this definition, from Edward Kmett's `constraints` package:

...

data Dict c where Dict :: c => Dict c

An `unsafeCoerce Dict` can be used to satisfy any arbitrary constraint.

Of course, it is often possible to use an inductive proof (er, recursive function) to produce Refl or Dict without resorting to unsafeCoerce. But, as the TypeLits Nat isn't inductive, we're forced to use drastic measures here.

Carter says:

...

I've been toying with the idea that the type lits syntax should be just that, a type level analogue of from integer that you can give to user land types, but I'm not going to suggest that till 7.8 is fully released.

I like this idea.

Christiaan says:

...

Iavor is working on a branch that allows the constraint solver to call an external solver: https://github.com/ghc/ghc/tree/decision-procedure

Yes, though I don't know how active this branch is currently. There are whispers afoot of going in the direction of strapping an SMT solver into GHC, though much work remains to be done before this happens. My sense is that an SMT solver will be necessary before TypeLits really becomes fluently useful. I'm confident this will happen eventually, but it may be over a year out, still. It's even possible that I will be the one to do it, but it's not on my short-to-do-list.

Christiaan says:

...

I myself worked on a patch that can only work with equalities: https://gist.github.com/christiaanb/8396614

Cool! Have you conferred with Iavor about this?

...

The current typeLits story for nats is kinda a fuster cluck to put it

Carter says: politely . We have type lits but we cant use them (well, we can't compute on them, which is the same thing).

I disagree on both counts here. TypeLits is a work in progress, as are many parts of GHC. That's one of the beautiful things about Haskell/GHC! Is there more progress to be made? Absolutely. But, without the work that's already been done, I'm not sure we would be as convinced as we are (still not 100%, to be sure, but getting there) that we need an SMT solver. We have to build on previous work, and to do that, we have to write potentially incomplete features. And, I've been able to use TypeLits most of the way toward implementing my `units` library (a way of type-checking with respect to units-of-measure). The only feature that they couldn't support was automatic unit conversions.

Carter says:

...

I'm still waiting (2 years later) for a solver we can actually include in ghc or even a user land solver!

I've done some thinking about user-land solvers and am quite interested in seeing it done. My chief thrust right now is about dependent types in Haskell, not this, but Iavor's "decision-procedure" branch lays a lot of the groundwork down for integrating perhaps multiple solvers in with GHC.

Henning says:

...

A minimal invasive solution would be to provide a kind for unary type level numbers and type functions that convert between Unary and Nat.

This definition is quite straightforward and works beautifully:

...

data Nat1 = Zero | Succ Nat1 type family U n where U 0 = Zero U n = Succ (U (n-1))

Iavor made sure that subtraction worked specifically in this case because it was so useful.

I hope this is helpful! Richard

On Mar 16, 2014, at 4:52 PM, Henning Thielemann < lemming@henning-thielemann.de> wrote:

...

Am 16.03.2014 20:02, schrieb Carter Schonwald:

...

respectfully, The current typeLits story for nats is kinda a fuster cluck to put it politely . We have type lits but we cant use them (well, we can't compute on them, which is the same thing).

For the past 2 years, every ghc release cycle, I first discover, then have to communicate to everyone else "you can't compute on type lits".

A minimal invasive solution would be to provide a kind for unary type level numbers and type functions that convert between Unary and Nat.

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

hrm, good point, that helps me understand this better, Thanks! On Tue, Mar 18, 2014 at 12:25 PM, Richard Eisenberg wrote:

I wouldn't call them unification queries against the constraint solver, because that implies a little more intelligence than is really there. They are unification queries, I suppose, against the fully-simplified (i.e., with as many type family simplifications as possible) arguments.

Pattern guards do not seem possible here, as unification (and *only* unification, nothing more complicated -- we couldn't handle it) plays a very central role to the mechanism. The theory is complicated enough as it is, and trying to add some form of guard (other than perhaps inequality guards, which play nicely with unification) would surely blow whatever small slice is left of the complexity budget.

Richard

On Mar 18, 2014, at 12:02 PM, Carter Schonwald wrote:

Would it be correct to think of closed type families as being more like a closed, ordered collection of unification queries against the constraint solver, that happens to act like pattern matching? Does that mean that one possible but potentially ill advised generalization be some sort of way to add pattern guards? I imagine it'd kinda work like instance heads for type classes. I'm not suggesting this mind you, merely thing to understand how to think about the crazy amount of power :)

that said, for fake 7.6 support i'm going to have to via CPP export the following opentype family :)

type family U (n:: LitNat) :: Nat -- can't induct, hence crippled type instance U n = Z

On Tue, Mar 18, 2014 at 9:33 AM, Richard Eisenberg wrote:

...

Yes, I suppose you would need UndecidableInstances. There's no way for GHC's (already rather weak) termination checker to know that by saying (n-1) a bunch, you're bound to reach 0.

I'm glad it's working for you. When I discovered this application for closed type families, I was rather pleased, myself!

Richard

On Mar 17, 2014, at 4:01 PM, Carter Schonwald wrote:

I had to enable undecidable instances, but I'm very very very happy with the U trick, no TH or other things needed. Thanks :)

On Mon, Mar 17, 2014 at 2:52 PM, Carter Schonwald < carter.schonwald@gmail.com> wrote:

...

(aside, pardon my earlier tone, been a bit overloaded the past few weeks, that crossed over to the list)

OOO that works? I guess that gives a decent way of using TypeLits as a concrete input syntax for Peano numbers. Thanks for pointing that out

I think i'm gonna go drop 7.6 support on some code i'm working on if this works :)

On Mon, Mar 17, 2014 at 2:05 PM, Richard Eisenberg wrote:

...

So much to respond to!

First, a little relevant context: Iavor Diatchki is the primary implementor of the type-lits stuff; I am not. But, he and I are playing in the same playground, so to speak, so we confer a fair amount and I may have some helpful perspective on all of this.

Henning asks:

...

How can I convince GHC that n+1 is always at least 1?

You can ramrod facts like this down GHC's throat when necessary. For example, the following works:

...

foo :: (1 <= n + 1) => Proxy n -> () foo _ = ()

lt :: Proxy n -> (1 <=? n + 1) :~: True lt _ = unsafeCoerce Refl

bar :: forall (n :: Nat). Proxy n -> () bar p = gcastWith (lt p) (foo p)

In case you're unfamiliar with them, here are some helpful definitions from Data.Type.Equality, used above:

...

data a :~: b where Refl :: a :~: a gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r

Also helpful when doing things like this is this definition, from Edward Kmett's `constraints` package:

...

data Dict c where Dict :: c => Dict c

An `unsafeCoerce Dict` can be used to satisfy any arbitrary constraint.

Of course, it is often possible to use an inductive proof (er, recursive function) to produce Refl or Dict without resorting to unsafeCoerce. But, as the TypeLits Nat isn't inductive, we're forced to use drastic measures here.

Carter says:

...

I've been toying with the idea that the type lits syntax should be just that, a type level analogue of from integer that you can give to user land types, but I'm not going to suggest that till 7.8 is fully released.

I like this idea.

Christiaan says:

...

Iavor is working on a branch that allows the constraint solver to call an external solver: https://github.com/ghc/ghc/tree/decision-procedure

Yes, though I don't know how active this branch is currently. There are whispers afoot of going in the direction of strapping an SMT solver into GHC, though much work remains to be done before this happens. My sense is that an SMT solver will be necessary before TypeLits really becomes fluently useful. I'm confident this will happen eventually, but it may be over a year out, still. It's even possible that I will be the one to do it, but it's not on my short-to-do-list.

Christiaan says:

...

I myself worked on a patch that can only work with equalities: https://gist.github.com/christiaanb/8396614

Cool! Have you conferred with Iavor about this?

...

The current typeLits story for nats is kinda a fuster cluck to put it

Carter says: politely . We have type lits but we cant use them (well, we can't compute on them, which is the same thing).

I disagree on both counts here. TypeLits is a work in progress, as are many parts of GHC. That's one of the beautiful things about Haskell/GHC! Is there more progress to be made? Absolutely. But, without the work that's already been done, I'm not sure we would be as convinced as we are (still not 100%, to be sure, but getting there) that we need an SMT solver. We have to build on previous work, and to do that, we have to write potentially incomplete features. And, I've been able to use TypeLits most of the way toward implementing my `units` library (a way of type-checking with respect to units-of-measure). The only feature that they couldn't support was automatic unit conversions.

Carter says:

...

I'm still waiting (2 years later) for a solver we can actually include in ghc or even a user land solver!

I've done some thinking about user-land solvers and am quite interested in seeing it done. My chief thrust right now is about dependent types in Haskell, not this, but Iavor's "decision-procedure" branch lays a lot of the groundwork down for integrating perhaps multiple solvers in with GHC.

Henning says:

...

A minimal invasive solution would be to provide a kind for unary type level numbers and type functions that convert between Unary and Nat.

This definition is quite straightforward and works beautifully:

...

data Nat1 = Zero | Succ Nat1 type family U n where U 0 = Zero U n = Succ (U (n-1))

Iavor made sure that subtraction worked specifically in this case because it was so useful.

I hope this is helpful! Richard

On Mar 16, 2014, at 4:52 PM, Henning Thielemann < lemming@henning-thielemann.de> wrote:

...

...

respectfully, The current typeLits story for nats is kinda a fuster cluck to put it politely . We have type lits but we cant use them (well, we can't compute on them, which is the same thing).

For the past 2 years, every ghc release cycle, I first discover, then have to communicate to everyone else "you can't compute on type

Am 16.03.2014 20:02, schrieb Carter Schonwald: lits".

A minimal invasive solution would be to provide a kind for unary type level numbers and type functions that convert between Unary and Nat.

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users