Hello Troels,<div>there is no solver included with ghc 7.6, if you wish to experiment with equational reasoning with the type level nats, you'll have to look into the ghc type-lits branch which includes a solver.</div>
<div><br></div><div>(yes, confusng, but true)<br><br><div class="gmail_quote">On Tue, Oct 2, 2012 at 2:54 PM, Troels Henriksen <span dir="ltr"><<a href="mailto:athas@sigkill.dk" target="_blank">athas@sigkill.dk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Consider the following definition of lists with a statically determined<br>
minimum length.<br>
<br>
data Nat' = Z | S Nat'<br>
<br>
data NList (n::Nat') a where<br>
Rest :: [a] -> NList Z a<br>
(:>) :: a -> NList n a -> NList (S n) a<br>
<br>
uncons :: NList (S n) a -> (a, NList n a)<br>
uncons (x :> xs) = (x, xs)<br>
<br>
This works fine. Now consider an implementation using the new type<br>
literals in GHC:<br>
<br>
data NList (n::Nat) a where<br>
Rest :: NList 0 [a]<br>
(:>) :: a -> NList n a -> NList (n+1) a<br>
<br>
uncons :: NList (n+1) a -> NList n a<br>
uncons (x :> l) = l<br>
<br>
This gives a type error:<br>
<br>
/home/athas/code/nonempty_lists.hs:41:19:<br>
Could not deduce (n1 ~ n)<br>
from the context ((n + 1) ~ (n1 + 1))<br>
bound by a pattern with constructor<br>
:> :: forall a (n :: Nat). a -> NList n a -> NList (n + 1) a,<br>
in an equation for `uncons'<br>
at /home/athas/code/nonempty_lists.hs:41:9-14<br>
`n1' is a rigid type variable bound by<br>
a pattern with constructor<br>
:> :: forall a (n :: Nat). a -> NList n a -> NList (n + 1) a,<br>
in an equation for `uncons'<br>
at /home/athas/code/nonempty_lists.hs:41:9<br>
`n' is a rigid type variable bound by<br>
the type signature for uncons :: NList (n + 1) a -> NList n a<br>
at /home/athas/code/nonempty_lists.hs:40:11<br>
Expected type: NList n a<br>
Actual type: NList n1 a<br>
In the expression: l<br>
In an equation for `uncons': uncons (x :> l) = l<br>
<br>
I don't understand why GHC cannot infer that the two types are the same.<br>
My guess is that 'n+1' is not "structural" to GHC in the same way that<br>
'S n' is. The page<br>
<a href="http://hackage.haskell.org/trac/ghc/wiki/TypeNats/MatchingOnNats" target="_blank">http://hackage.haskell.org/trac/ghc/wiki/TypeNats/MatchingOnNats</a><br>
mentions that "type level numbers of kind Nat have no structure", which<br>
seems to support my suspicion. What's the complete story, though?<br>
<span class="HOEnZb"><font color="#888888"><br>
--<br>
\ Troels<br>
/\ Henriksen<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</font></span></blockquote></div><br></div>