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

[adam vogt]

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 <v.dijk.bas at gmail.com> 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150506/bcd11972/attachment.html>