Strange things with type literals of kind Nat
Consider the following definition of lists with a statically determined minimum length. data Nat' = Z | S Nat' data NList (n::Nat') a where Rest :: [a] -> NList Z a (:>) :: a -> NList n a -> NList (S n) a uncons :: NList (S n) a -> (a, NList n a) uncons (x :> xs) = (x, xs) This works fine. Now consider an implementation using the new type literals in GHC: data NList (n::Nat) a where Rest :: NList 0 [a] (:>) :: a -> NList n a -> NList (n+1) a uncons :: NList (n+1) a -> NList n a uncons (x :> l) = l This gives a type error: /home/athas/code/nonempty_lists.hs:41:19: Could not deduce (n1 ~ n) from the context ((n + 1) ~ (n1 + 1)) bound by a pattern with constructor :> :: forall a (n :: Nat). a -> NList n a -> NList (n + 1) a, in an equation for `uncons' at /home/athas/code/nonempty_lists.hs:41:9-14 `n1' is a rigid type variable bound by a pattern with constructor :> :: forall a (n :: Nat). a -> NList n a -> NList (n + 1) a, in an equation for `uncons' at /home/athas/code/nonempty_lists.hs:41:9 `n' is a rigid type variable bound by the type signature for uncons :: NList (n + 1) a -> NList n a at /home/athas/code/nonempty_lists.hs:40:11 Expected type: NList n a Actual type: NList n1 a In the expression: l In an equation for `uncons': uncons (x :> l) = l I don't understand why GHC cannot infer that the two types are the same. My guess is that 'n+1' is not "structural" to GHC in the same way that 'S n' is. The page http://hackage.haskell.org/trac/ghc/wiki/TypeNats/MatchingOnNats mentions that "type level numbers of kind Nat have no structure", which seems to support my suspicion. What's the complete story, though? -- \ Troels /\ Henriksen
Hello Troels,
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.
(yes, confusng, but true)
On Tue, Oct 2, 2012 at 2:54 PM, Troels Henriksen
Consider the following definition of lists with a statically determined minimum length.
data Nat' = Z | S Nat'
data NList (n::Nat') a where Rest :: [a] -> NList Z a (:>) :: a -> NList n a -> NList (S n) a
uncons :: NList (S n) a -> (a, NList n a) uncons (x :> xs) = (x, xs)
This works fine. Now consider an implementation using the new type literals in GHC:
data NList (n::Nat) a where Rest :: NList 0 [a] (:>) :: a -> NList n a -> NList (n+1) a
uncons :: NList (n+1) a -> NList n a uncons (x :> l) = l
This gives a type error:
/home/athas/code/nonempty_lists.hs:41:19: Could not deduce (n1 ~ n) from the context ((n + 1) ~ (n1 + 1)) bound by a pattern with constructor :> :: forall a (n :: Nat). a -> NList n a -> NList (n + 1) a, in an equation for `uncons' at /home/athas/code/nonempty_lists.hs:41:9-14 `n1' is a rigid type variable bound by a pattern with constructor :> :: forall a (n :: Nat). a -> NList n a -> NList (n + 1) a, in an equation for `uncons' at /home/athas/code/nonempty_lists.hs:41:9 `n' is a rigid type variable bound by the type signature for uncons :: NList (n + 1) a -> NList n a at /home/athas/code/nonempty_lists.hs:40:11 Expected type: NList n a Actual type: NList n1 a In the expression: l In an equation for `uncons': uncons (x :> l) = l
I don't understand why GHC cannot infer that the two types are the same. My guess is that 'n+1' is not "structural" to GHC in the same way that 'S n' is. The page http://hackage.haskell.org/trac/ghc/wiki/TypeNats/MatchingOnNats mentions that "type level numbers of kind Nat have no structure", which seems to support my suspicion. What's the complete story, though?
-- \ Troels /\ Henriksen
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (2)
-
Carter Schonwald -
Troels Henriksen