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 Hello, I've been thinking of the design (an implementation) for the type naturals as consisting of two stages. I am quite happy with the first stage and it was working pretty well a few months ago, so hopefully I can get it back in shape soon. This is the code that I'd like to integrate into the main branch because I think that any other work on type naturals is likely to have to do at least that part. The second stage involves a more advanced solver (and the UNat and BNat types, etc).--- I've been working on it for a while but I don't think it is quite ready yet. So here is some more details about what's in stage 1: - A new kind for natural numbers, called Nat. It is only a sub-kind of itself. - An infinite family of types, one for each natural number (0, 1, 2, etc). As we discussed before, this is implemented as new data constructor in GHC's type for types, so the implementation touches many files. - A family of singleton types (also called Nat :: Nat -> *), linking the type level to the value level. For example, there is only one value of type "Nat 3", namely the number 3. This is achieved via a built-in overloaded constructor for the singletons. (There is more explanation of how this works ob the wiki, please ask me if it seems confusing). - Support for treating all operators at the type level as type constructors. This means that operators like (+), (*), etc can be used as the names of datatypes and type functions (in the current GHC they are type variables). This required a small extension to the module system, so that we can distinguish between exporting (+) the value, and (+) the type function. With the extension that I implemented, in module imports or exports we write "type (+)" or "(+)()" to indicate that we are referring to something in the type/calss name-space rather then the value name-space. - A set of operations on the natural number types: type functions for addition (+), multiplication (*), and exponentiation (*), and a 2-parameter class (<=) for comparisons. These are built-into GHC in that there are checks that programmers cannot provide additional instances for them, and there are hooks in the solver to solve these. I think that for stage 1 we should only have a simple solver that has hardly any symbolic solving, and leave a nicer solver (something like what's described in my e-mail to Adam bellow, or perhaps something different) for stage 2. In my experience, even the simple solver works well, as long as one uses a certain programming style. So here are my thoughts on Simon's questions: On Tue, Jun 7, 2011 at 2:54 AM, Simon Peyton-Jones <[email protected]<mailto:[email protected]>> wrote: Iavor, and others interested in type-level arithmetic I’d been meaning to get in touch with you to ask about when would be a good moment to merge your work into the GHC master branch. • How satisfied are you with the design? Is it one point among many, or does it feel “right”. Eg Nat, UNat and BNat seem a bit complicated to me... (I know that that the exact power of the solver is a moveable feast.) I am quite happy with the design of stage 1. I suspect that, at least in the context of Haskell, adding type naturals would involve adding the things that I outlined above. • How well does it integrate with GHC’s new type constraint solver? Dimitrios is the expert here. I tried to make that part quite modular, as I've changed it quite a few times since I started working. Currently, the type-naturals solver is in a completely separate module, which is hooked into GHC's solver as a separate "pass". • How do you deal with the evidence generation stuff and System FC? The evidence for the type naturals can be grouped into three classes: - Evidence for class "NatI". This is the class that links type-level naturals to value level naturals. The "dictionary" for this class is just an integer corresponding to the number which is being made. (I think that there is more about how this works on the type naturals wiki). - 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. In general I’d be happy to have it in the master branch, if the design seems stable and the code is modular (notably, I assume that the arithmetic constraint solver is cleanly separable). Yes, the arithmetic solver is quite separate. Adding the type-natural literals is not at all modular though, because it modifies a datatype, and so I had to add a new case to all the functions that work on the datatype. So merging this part in would make maintenance a lot simpler. Hope this helps, -Iavor From: Iavor Diatchki [mailto:[email protected]<mailto:[email protected]>] Sent: 03 June 2011 16:18 To: Adam Gundry Cc: Simon Peyton-Jones Subject: Re: Type-level natural numbers Hi Adam, For the last few months I've been playing around with different ways of improving the solver, but that's outside the GHC tree, so it is likely that my changes to GHC have bit-rotted. I'll have a go at updating things and perhaps touch bases with GHC HQ, to try to get what's in the repo merged in the main branch, so that it does not keep breaking all the time. Also, I'd be interested to hear more about your ideas (theory is important!). My latest attempt (which is not in the GHC sources yet) is to try to write th solver as an LCF style theorem prover, thinking that if I can get this to work it would be quite flexible and general, and we can experiment with different basic sets of axioms and inference techniques. The current set of properties I'd like to teach GHC (but it is not working yet :( ) is: - (+,0) is a commutative monoid - (*,1) is a commutative monoid - 0 annihilates * - left and right cancellation laws (i.e., the backward FDs): - (a + b = c, a' + b = c) => (a = a') - (a * b = c, a' * b = c, 1 <= b) => (a = a') -- i.e., division - (a ^ b = c, a' ^ b = c, 1 <= b) => (a = a') -- i.e., taking N-th root - (a ^ b = c, a ^ b' = c, 2 <= a) => (b = b') -- i.e., taking logs - distributivity rules: - a * (b + c) = a * c + b * c, - (a * b) ^ c = a ^ c * b ^ c - a ^ (b + c) = a ^ b + a ^ c - power rule: a ^ (b * c) = (a ^ b) ^ c I use singleton types to link the type-level naturals with the values level. While playing around with various examples, I found that it is useful to have two additional families of singleton types, to support different styles of inductive definitions. So beside the basic singleton family, I also use the following two families: -- Useful for inductive list-like definitions. data UNat :: Nat -> * where Zero :: UNat 0 -> UNat (n + 1) Succ :: UNat n -- Useful for inductive tree-like definitions (some bit algorithms use things like that) data BNat :: Nat -> * where BZero :: UNat 0 Odd :: BNat n -> BNat (2 * n + 1) Even :: (1 <= n) => BNat n -> BNat (2 * n) There are also built-in functions to "view" the basic singleton family into these forms: toUNat :: Nat n -> UNat n toBNat :: Nat n -> BNat n One could probably think of better names for many of these... Well, this e-mail got quite long, sorry about that, and I hope that it is useful, -Iavor PS: Please feel free to ask questions if things are unclear, or suggest different approaches. On Fri, Jun 3, 2011 at 1:37 AM, Adam Gundry <[email protected]<mailto:[email protected]>> wrote: > > Dear Iavor, > > I have been following your work on the type-level naturals extension to > GHC with interest, and was wondering how things are going? I would like > to try out the extension, but, since some of the GHC repositories > switched to Git, I've been struggling to construct a version with your > recent patches that will compile. What's the best way to check out a > copy of your code? Are there any more recent repositories than those > listed on the Trac ticket (http://hackage.haskell.org/trac/ghc/ticket/4385)? > > You may recall that we met at ICFP last year. I am working on type-level > numbers for Haskell, though with more of a focus on the theory and > issues relating to type inference. At the moment I'm writing a paper > examining the design choices involved. I think it would be good for us > to keep in touch on progress, so we can pull in the same direction. > > Best regards, > > Adam Gundry > > > -- > PhD Student > University of Strathclyde
_______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
