#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 pumpkin):
I'm wondering what is planned regarding support for ad-hoc "proofs".
Although the solver is looking awesome, the general case of automatically
solving (quantified) statements about naturals with addition,
multiplication (boo), and order is undecidable. If I (taking as an example
the memory-arrays repository) had a complex index calculation that led to
the automatic solver not being able to determine that my numbers unify,
what can I do to convince it? Does unsafeCoerce do the right thing on
naturals? Can I compose small fundamental principles of natural arithmetic
that the solver does understand to build up a larger proof, as one might
do in an actual proof language? If so, will the construction of the proof
have a runtime cost, or can it all be cleverly erased at runtime?
I apologize if these questions are answered elsewhere, but I was unable to
see anything much covering them.
I'm very excited by this development and look forward to tinkering with it
as soon as I get some time, so thanks!
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4385#comment:15>
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
