positive type-level naturals

Tue Mar 18 16:02:30 UTC 2014

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/64fc0a60/attachment-0001.html>