positive type-level naturals

[Carter Schonwald]

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/20140317/98d09d73/attachment-0001.html>