[Haskell-cafe] How to define a type-level append?

[Bas van Dijk]

Hi,

At the bottom I have a type-level programming related
question, but first some preliminaries:

> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE TypeOperators #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE DataKinds #-}
>
> import GHC.TypeLits

I've implemented a protocol where a client can send a packet
of orders to a server. An OrderPacket is either empty
(represented by the "NoOrders" constructor) or consists of
an Order and possibly more orders (represented by the:
"order :> orders" constructor).

An Order is defined by a type-level list of numeric
addresses and a command. The semantics is that the server
should address the command to the list of addresses.

When the client sends a packet of orders, the server has to
return a reply for each command for each address in order. I
lifted this expectation into the type signature so that when
the client sends an order the type-checker will complain if
it tries to pattern match on the wrong reply.

The above is formalized with the following GADT for a packet
of orders (I left out some off-topic stuff):

> data OrderPacket replies where
>     NoOrders :: OrderPacket '[]
>     (:>) :: !(Order addrs cmd)
>          -> !(OrderPacket replies)
>          -> OrderPacket
>               (RepliesFor addrs cmd :++: replies)
>
> infixr 5 :>
>
> data Order (addrs :: [Nat]) command where
>     Order :: (Command command)
>           => !command -> Order addrs command
>
> class Command command where
>     type Response command :: *
>     -- I left out some encoding/decoding related methods.
>
> type family RepliesFor (addrs :: [Nat])
>                        (cmd :: *) :: [*] where
>     RepliesFor '[]             cmd = '[]
>     RepliesFor (addr ': addrs) cmd =
>         Reply addr cmd ': RepliesFor addrs cmd
>
> type family (xs :: [*]) :++: (ys :: [*]) :: [*] where
>   '[]       :++: ys = ys
>   (x ': xs) :++: ys = x ': (xs :++: ys)
>
> infixr 5 :++:
>
> data Reply (addr :: Nat) command =
>     Response !(Maybe (Response command))
>     -- I left out some other stuff that can be in a reply.
>

Now my problem, I would like to have the ability to append
two OrderPackets. I would say the following type properly
reflects what I want:

> append :: OrderPacket replies1
>        -> OrderPacket replies2
>        -> OrderPacket (replies1 :++: replies2)

How would I implement this? The following naive defintion

> append NoOrders  ys = ys
> append (x :> xs) ys = x :> append xs ys

gives the following type error:

src/Test.lhs:77:25:
  Could not deduce ((RepliesFor addrs cmd
                     :++: (replies :++: replies2))
                    ~ (replies1 :++: replies2))
  from the context
    (replies1 ~ (RepliesFor addrs cmd :++: replies))
    bound by a pattern with constructor
        :> :: forall (addrs :: [Nat]) cmd (replies :: [*]).
              Order addrs cmd
              -> OrderPacket replies
              -> OrderPacket
                   (RepliesFor addrs cmd :++: replies),
      in an equation for ‘append’
    at src/Test.lhs:77:11-17
  NB: ‘:++:’ is a type function, and may not be injective
  Expected type: OrderPacket (replies1 :++: replies2)
    Actual type: OrderPacket
                   (RepliesFor addrs cmd :++:
                     (replies :++: replies2))
  Relevant bindings include
    ys :: OrderPacket replies2 (bound at src/Test.lhs:77:20)
    xs :: OrderPacket replies (bound at src/Test.lhs:77:16)
    x :: Order addrs cmd (bound at src/Test.lhs:77:11)
    append :: OrderPacket replies1
              -> OrderPacket replies2
              -> OrderPacket (replies1 :++: replies2)
      (bound at src/Test.lhs:76:3)
  In the expression: x :> append xs ys
  In an equation for ‘append’:
      append (x :> xs) ys = x :> append xs ys

I suspect I need to adapt the type signature of "append" to suite the
definition.

Cheers,

Bas