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.) · How well does it integrate with GHC’s new type constraint solver? Dimitrios is the expert here. · How do you deal with the evidence generation stuff and System FC? 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). Simon From: Iavor Diatchki [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
