<div dir="ltr"><div>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 :) </div>
<div><br></div>that said, for fake 7.6 support i'm going to have to via CPP export the following opentype family :) <div><div><br></div><div>type family U (n:: LitNat) :: Nat</div><div>-- can't induct, hence crippled</div>
<div>type instance U n = Z </div></div><div><br></div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Mar 18, 2014 at 9:33 AM, Richard Eisenberg <span dir="ltr"><<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word"><div>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.</div>
<div><br></div><div>I'm glad it's working for you. When I discovered this application for closed type families, I was rather pleased, myself!</div><span class="HOEnZb"><font color="#888888"><div><br></div><div>Richard</div>
</font></span><div><div class="h5"><br><div><div>On Mar 17, 2014, at 4:01 PM, Carter Schonwald wrote:</div><br><blockquote type="cite"><div dir="ltr">I had to enable undecidable instances, but I'm very very very happy with the U trick, no TH or other things needed. Thanks :) </div>
<div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Mar 17, 2014 at 2:52 PM, Carter Schonwald <span dir="ltr"><<a href="mailto:carter.schonwald@gmail.com" target="_blank">carter.schonwald@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>(aside, pardon my earlier tone, been a bit overloaded the past few weeks, that crossed over to the list)</div>
<div><br></div>OOO<div>that works? </div><div>I guess that gives a decent way of using TypeLits as a concrete input syntax for Peano numbers. Thanks for pointing that out</div>
<div><br></div><div>I think i'm gonna go drop 7.6 support on some code i'm working on if this works :) </div><div><br></div><div><br></div><div><br></div></div><div><div><div class="gmail_extra">
<br><br><div class="gmail_quote">
On Mon, Mar 17, 2014 at 2:05 PM, Richard Eisenberg <span dir="ltr"><<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
So much to respond to!<br>
<br>
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.<br>
<br>
Henning asks:<br>
<div>> How can I convince GHC that n+1 is always at least 1?<br>
<br>
</div>You can ramrod facts like this down GHC's throat when necessary. For example, the following works:<br>
<br>
> foo :: (1 <= n + 1) => Proxy n -> ()<br>
> foo _ = ()<br>
><br>
> lt :: Proxy n -> (1 <=? n + 1) :~: True<br>
> lt _ = unsafeCoerce Refl<br>
><br>
> bar :: forall (n :: Nat). Proxy n -> ()<br>
> bar p = gcastWith (lt p) (foo p)<br>
<br>
<br>
In case you're unfamiliar with them, here are some helpful definitions from Data.Type.Equality, used above:<br>
<br>
> data a :~: b where<br>
> Refl :: a :~: a<br>
> gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r<br>
<br>
Also helpful when doing things like this is this definition, from Edward Kmett's `constraints` package:<br>
<br>
> data Dict c where<br>
> Dict :: c => Dict c<br>
<br>
An `unsafeCoerce Dict` can be used to satisfy any arbitrary constraint.<br>
<br>
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.<br>
<div><br>
Carter says:<br>
> 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.<br>
<br>
<br>
</div>I like this idea.<br>
<div><br>
Christiaan says:<br>
> Iavor is working on a branch that allows the constraint solver to call an external solver: <a href="https://github.com/ghc/ghc/tree/decision-procedure" target="_blank">https://github.com/ghc/ghc/tree/decision-procedure</a><br>
<br>
<br>
</div>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.<br>
<div><br>
Christiaan says:<br>
> I myself worked on a patch that can only work with equalities: <a href="https://gist.github.com/christiaanb/8396614" target="_blank">https://gist.github.com/christiaanb/8396614</a><br>
<br>
<br>
</div>Cool! Have you conferred with Iavor about this?<br>
<div><br>
Carter says:<br>
> 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).<br>
<br>
</div>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.<br>
<div><br>
Carter says:<br>
> I'm still waiting (2 years later) for a solver we can actually include in ghc or even a user land solver!<br>
<br>
<br>
</div>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.<br>
<div><br>
Henning says:<br>
> A minimal invasive solution would be to provide a kind for unary type level numbers and type functions that convert between Unary and Nat.<br>
<br>
<br>
</div>This definition is quite straightforward and works beautifully:<br>
<br>
> data Nat1 = Zero | Succ Nat1<br>
> type family U n where<br>
> U 0 = Zero<br>
> U n = Succ (U (n-1))<br>
<br>
Iavor made sure that subtraction worked specifically in this case because it was so useful.<br>
<br>
I hope this is helpful!<br>
<span><font color="#888888">Richard<br>
</font></span><div><div><br>
On Mar 16, 2014, at 4:52 PM, Henning Thielemann <<a href="mailto:lemming@henning-thielemann.de" target="_blank">lemming@henning-thielemann.de</a>> wrote:<br>
<br>
> Am 16.03.2014 20:02, schrieb Carter Schonwald:<br>
>> respectfully,<br>
>> The current typeLits story for nats is kinda a fuster cluck to put it<br>
>> politely . We have type lits but we cant use them (well, we can't<br>
>> compute on them, which is the same thing).<br>
>><br>
>> For the past 2 years, every ghc release cycle, I first discover, then<br>
>> have to communicate to everyone else "you can't compute on type lits".<br>
><br>
> A minimal invasive solution would be to provide a kind for unary type level numbers and type functions that convert between Unary and Nat.<br>
><br>
</div></div><div><div>> _______________________________________________<br>
> Glasgow-haskell-users mailing list<br>
> <a href="mailto:Glasgow-haskell-users@haskell.org" target="_blank">Glasgow-haskell-users@haskell.org</a><br>
> <a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users</a><br>
<br>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>
</blockquote></div><br></div></div></div></blockquote></div><br></div>