#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 adamgundry):
Nice work! It's good to see some progress in this direction.
We should certainly think about how users can provide more information to
the constraint solver, either as explicit proofs or perhaps hints about
useful lemmas to guide the search process. I'm not convinced that changing
or removing type signatures on the whim of the compiler is a good
strategy. (Can we even infer types properly for these things?)
I have been experimenting with the version of 9th January (while I try to
figure out how to check out and build a more up to date version), so
apologies if the following is a bit out of date. Perhaps I'm missing
something, but I can't make the following classic example work:
{{{
data Vec :: Nat -> * -> * where
Nil :: Vec 0 a
(:>) :: a -> Vec n a -> Vec (n+1) a
(+++) :: Vec n a -> Vec m a -> Vec (n+m) a
Nil +++ bs = bs
(a :> as) +++ bs = a :> (as +++ bs)
}}}
In the last line, the solver fails to deduce ((1 + (n1 + m)) ~ (n + m))
from the context (n ~ (n1 + 1)). One use of unsafeCoerce is enough to get
it accepted, but I can't see how two modify the type signature to make
this go through. My point is not so much that this example fails, as the
solver could presumably be extended to make it work, but that in general
such problems will occur.
My perspective is from working with dependent types and inductive families
(GADTs). I think that a lot of the interest in type-level numbers comes
from their use along with GADTs, as pumpkin's example indicates, so we
need to figure out how the interaction between the two will work.
One final thought: at the moment there doesn't seem to be any way to
pattern match on numbers, at least without using natToInteger and so
discarding statically-known information. For example, the Applicative
functor instance for vectors includes
{{{
pure :: Nat n -> a -> Vec n a
}}}
which makes a vector full of a single value. At the moment, the
implementation by pattern-matching and recursion on the first argument
doesn't seem to be possible in a type-safe way. One can add a unary
representation of numbers indexed by their Nat values inside the TypeNats
module abstraction barrier, but this is a bit clunky and inefficient.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4385#comment:18>
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
