#4385: Type-level natural numbers
----------------------------------------+-----------------------------------
Reporter: diatchki | Owner: diatchki
Type: feature request | Status: new
Priority: normal | Milestone: 7.2.1
Component: Compiler (Type checker) | Version:
Keywords: | Testcase:
Blockedby: | Difficulty:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
----------------------------------------+-----------------------------------
Comment(by diatchki):
Hello,
I am certainly still working on it, and I think that it'd be great to
merge it with HEAD. What would be the best way to work on the design
issues---I feel that these ticket comments do not have enough space to
discuss things properly. Perhaps I will make a page on the wiki where we
(meaning whoever is interested in this feature) can list all the issues
and see how to solve them best? I'll update the ticket when I get a
chance to do this.
Briefly, my current status is:
- I've added the syntactic change to treat all symbols as type
constructors, and the associated change to the module system. In the
process I noticed that GHC does not really use the precedence machinery
for infix predicates (classes, ~). Adding support for this is on my TODO
list, so that we can write things like `(a + b ~ c)`, rather then `((a +
b) ~ c)`.
- I've implemented the numeric type literals, which are of a new kind
(currently called) Nat. I've added a new form of type `LiteralTy TyLit`,
where `TyLit` is a type for type-level literals. Currently, it has only
numbers in it but later we could add other things too, if we deemed it
useful.
- I've added a set of operations on the type numbers, currently:
comparison `(<=)`, addition `(+)`, multiplication `(*)`, and
exponentiation `(^)`. By using equality constraints, we also get their
inverses: subtraction, division, logarithms, and roots. My solver is by
no means complete although it seems to work for a number of practical
examples. I am sure that we can continue to improve it for a long time
though.
The current implementation cheats on the proofs for the equalities and
(<=) because it uses "unsafeCoercions". At first I had it generate proofs
but then you mentioned that you were redoing the evidence mechanism based
on Brent's work, and the proofs were getting quite large and difficult to
read so I removed them. It would not be hard to re-add them but we should
decide on the granularity of the primitive axioms (coercions) to use. The
trade-off is basically RISC vs CISC, a smaller set of simpler axioms tends
to result in larger proofs.
There is also an issue about what evidence to pass for (<=). (<=) is
similar to (~) (and any other class with no methods) in that it does not
really need any runtime evidence. I could not see how to adopt the (~)
mechanism to account for (<=) so, currently, the evidence for (<=) is
basically a hack (the run-time evidence calls error if it is ever
evaluated). It might be nice if we had a unified way to treat things
without evidence (e.g., by having a special form of argument that does not
emit any run-time code) but I have not looked into how hard would be to do
this. Can anyone think of a better way to do this?
- In the support library, I made the `DynNat` change that Simon
described above. This worked out really nice because this type is
basically the type of natural numbers at the value level, so I added all
the usual instances for it and called it `Natural`, which mirrors
`Integer`.
I think that that's all.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4385#comment:9>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
