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
