positive type-level naturals

[Richard Eisenberg]

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 <lemming at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users