#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
----------------------------------------+-----------------------------------
Changes (by simonpj):
* cc: sweir...@…, dimit...@…, byor...@…, conor.mcbr...@… (added)
Comment:
Good! My suggestions for progress:
* Keep an up-to-date (preferably wiki) description of the users-eye view
of the system. You had this before, but it may need updating eg with
`DynNat`.
* Keep a wiki page, as you suggest, summarising design issues.
You already have these, I think, here
http://hackage.haskell.org/trac/ghc/wiki/TypeNats, although the division
between "user manual", "design issues", and "implemetation notes" isn't
very clear. Especially important is to summarise open design and
implementation issues.
Email discussion belongs on cvs-ghc, I guess?
Concerning evidence, as soon as I get the new typechecker settled down I'm
going to work on the evidence part of FC. In particular, equality
evidence is currently treated like types, and erased, in contrast to class
evidence which is not erased and is passed at runtime. I have a plan to
treat both uniformly, not ''erasing'' equality evidence, but rather
treating it as a value like the "state token" of the state monad. That
is, a value that can be passed around in zero bits. This will make
everying much nicer and more uniform.
Still the question remains of what evidence terms FC should have for
numerics.
Iavor, if you continue to drive this, I'll be responsive. I'm adding
Stephanie, Brent, Conor, Dimitrios to the cc list.
Simon
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4385#comment:10>
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
