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

6 May 2015

      Hi Adam,

Both seem like good ideas. I will try which one works best and report back.

Thanks!

Bas

On 6 May 2015 at 17:39, adam vogt  wrote:
...
Hi Bas,
Seems to be that ghc needs help to see that :++: is associative.
http://lpaste.net/2511796689740759040 is one way to show that. Alternatively
you could make append a class, which lets ghc figure out
((RepliesFor addrs cmd
                     :++: (replies :++: replies2))
                    ~ (replies1 :++: replies2))
later on: when the actual elements of the lists are known I think ghc may be
able to see that both sides of the ~ simplify to the same type.
Regards,
Adam
On Wed, May 6, 2015 at 7:11 AM, Bas van Dijk  wrote:
...
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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe