On Thu, Jun 23, 2011 at 3:34 PM, Simon Peyton-Jones <[email protected]> wrote: > Iavor > > > > Thanks for putting it in the GHC repo. > > > > Dimtrios has an intern starting in a week. We plan to work on adding kinds > to GHC, which is in very much the same territory as you’ve been working in > . So I think we’ll look carefully at your stuff over the next month or two. > > > > To me the big open question is the one of what evidence we want to track. > We can bale out and have a “trust-me” evidence constant, and that’s probably > appropriate at some point. One could a similar question about, say, > Kennedy-style dimension types. > > > > Simon > > > > From: Iavor Diatchki [mailto:[email protected]] > Sent: 11 June 2011 20:33 > To: Simon Peyton-Jones > Cc: Adam Gundry; Dimitrios Vytiniotis; [email protected]; Conor McBride; > Stephanie Weirich > Subject: Re: Type-level natural numbers > > > > [...] > > > - Evidence for the class "<=". This class has no methods, so we don't > need any run-time evidence. In principle, we could pass around a proof but > this just seems like wasted work, although perhaps it could be useful for > debugging? My current implementation passes a thunk that will throw an > error if it is ever evaluated, as this would indicate a bug. > > > > - Evidence for equalities involving the +,*,^ type functions. My current > solver cheats on this one, and just adds coercions when it proves something. > Clearly, this is not very good. I made this choice for the following > reasons: > > * The pragmatic (perhaps not very good) reason was that the solver uses > many rules, and the proofs can get quite large, so looking at them was not > really useful. So I thought that adding a whole bunch of coercsions would > just complicate things without much benefit. I found that adding various > traces in the solver was good enough for debugging but, of course, having > proof objects could help with much more extensive testing. In the longer > run, I think that it might be nice to write the solver in an LCF style > (theorems are an abstract type) and then it should not be hard to turn proof > recording on and off. > > * The more technical reason is that some of the rules do not fit in FC > because equality is treated differently from other predicates. For example, > consider the left cancellation law for multiplication: > > (a * b1 = c, a * b2 = c, 1 <= a) => (b1 = b2) > > > > Here we need the side-condition that "1 <= a" so that we don't divide by 0. > The problem is that "<=" is a class, while rest are coercions.
At the risk of making a fool of myself by sticking my nose into things I don't fully understand, this could potentially be solved by adding type-level True and False of kind Bool, turning <= into a type function Nat -> Nat -> Bool, and then using constraints of the form ((n <= m) ~ True). Presumably you've considered this, and there's a good reason to go with (<=) as a class instead? _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
