positive type-level naturals

Tue Mar 18 16:32:53 UTC 2014

hrm, good point, that helps me understand this better, Thanks!

On Tue, Mar 18, 2014 at 12:25 PM, Richard Eisenberg <eir at cis.upenn.edu>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 <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/342bc5df/attachment-0001.html>