Troels Henriksen | 2 Oct 20:54 2012
Picon

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'
(Continue reading)

Carter Schonwald | 3 Oct 06:22 2012
Picon

Re: Strange things with type literals of kind Nat

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 <athas <at> sigkill.dk> wrote:
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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane