positive type-level naturals

Tue Mar 18 16:25:56 UTC 2014

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 <eir at cis.upenn.edu> 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 at 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 <eir at cis.upenn.edu> 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?
>> 
>> 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
>> 
>> 
>> 
> 
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20140318/3adabf09/attachment.html>