hrm, good point, that helps me understand this better, Thanks!
On Tue, Mar 18, 2014 at 12:25 PM, Richard Eisenberg <e...@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 <e...@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.schonw...@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 >>> <e...@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 < >>>> lemm...@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@haskell.org >>>> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >>>> >>>> >>> >> >> > >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
