<div dir="ltr"><div><div><div><div>Hi Bas,<br><br></div>Seems to be that ghc needs help to see that :++: is associative. <a href="http://lpaste.net/2511796689740759040">http://lpaste.net/2511796689740759040</a> is one way to show that. Alternatively you could make append a class, which lets ghc figure out<br><br>((RepliesFor addrs cmd<br>
:++: (replies :++: replies2))<br>
~ (replies1 :++: replies2))<br><br></div>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.<br><br></div>Regards,<br></div>Adam<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, May 6, 2015 at 7:11 AM, Bas van Dijk <span dir="ltr"><<a href="mailto:v.dijk.bas@gmail.com" target="_blank">v.dijk.bas@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
At the bottom I have a type-level programming related<br>
question, but first some preliminaries:<br>
<br>
> {-# LANGUAGE GADTs #-}<br>
> {-# LANGUAGE TypeOperators #-}<br>
> {-# LANGUAGE TypeFamilies #-}<br>
> {-# LANGUAGE DataKinds #-}<br>
><br>
> import GHC.TypeLits<br>
<br>
I've implemented a protocol where a client can send a packet<br>
of orders to a server. An OrderPacket is either empty<br>
(represented by the "NoOrders" constructor) or consists of<br>
an Order and possibly more orders (represented by the:<br>
"order :> orders" constructor).<br>
<br>
An Order is defined by a type-level list of numeric<br>
addresses and a command. The semantics is that the server<br>
should address the command to the list of addresses.<br>
<br>
When the client sends a packet of orders, the server has to<br>
return a reply for each command for each address in order. I<br>
lifted this expectation into the type signature so that when<br>
the client sends an order the type-checker will complain if<br>
it tries to pattern match on the wrong reply.<br>
<br>
The above is formalized with the following GADT for a packet<br>
of orders (I left out some off-topic stuff):<br>
<br>
> data OrderPacket replies where<br>
> NoOrders :: OrderPacket '[]<br>
> (:>) :: !(Order addrs cmd)<br>
> -> !(OrderPacket replies)<br>
> -> OrderPacket<br>
> (RepliesFor addrs cmd :++: replies)<br>
><br>
> infixr 5 :><br>
><br>
> data Order (addrs :: [Nat]) command where<br>
> Order :: (Command command)<br>
> => !command -> Order addrs command<br>
><br>
> class Command command where<br>
> type Response command :: *<br>
> -- I left out some encoding/decoding related methods.<br>
><br>
> type family RepliesFor (addrs :: [Nat])<br>
> (cmd :: *) :: [*] where<br>
> RepliesFor '[] cmd = '[]<br>
> RepliesFor (addr ': addrs) cmd =<br>
> Reply addr cmd ': RepliesFor addrs cmd<br>
><br>
> type family (xs :: [*]) :++: (ys :: [*]) :: [*] where<br>
> '[] :++: ys = ys<br>
> (x ': xs) :++: ys = x ': (xs :++: ys)<br>
><br>
> infixr 5 :++:<br>
><br>
> data Reply (addr :: Nat) command =<br>
> Response !(Maybe (Response command))<br>
> -- I left out some other stuff that can be in a reply.<br>
><br>
<br>
Now my problem, I would like to have the ability to append<br>
two OrderPackets. I would say the following type properly<br>
reflects what I want:<br>
<br>
> append :: OrderPacket replies1<br>
> -> OrderPacket replies2<br>
> -> OrderPacket (replies1 :++: replies2)<br>
<br>
How would I implement this? The following naive defintion<br>
<br>
> append NoOrders ys = ys<br>
> append (x :> xs) ys = x :> append xs ys<br>
<br>
gives the following type error:<br>
<br>
src/Test.lhs:77:25:<br>
Could not deduce ((RepliesFor addrs cmd<br>
:++: (replies :++: replies2))<br>
~ (replies1 :++: replies2))<br>
from the context<br>
(replies1 ~ (RepliesFor addrs cmd :++: replies))<br>
bound by a pattern with constructor<br>
:> :: forall (addrs :: [Nat]) cmd (replies :: [*]).<br>
Order addrs cmd<br>
-> OrderPacket replies<br>
-> OrderPacket<br>
(RepliesFor addrs cmd :++: replies),<br>
in an equation for ‘append’<br>
at src/Test.lhs:77:11-17<br>
NB: ‘:++:’ is a type function, and may not be injective<br>
Expected type: OrderPacket (replies1 :++: replies2)<br>
Actual type: OrderPacket<br>
(RepliesFor addrs cmd :++:<br>
(replies :++: replies2))<br>
Relevant bindings include<br>
ys :: OrderPacket replies2 (bound at src/Test.lhs:77:20)<br>
xs :: OrderPacket replies (bound at src/Test.lhs:77:16)<br>
x :: Order addrs cmd (bound at src/Test.lhs:77:11)<br>
append :: OrderPacket replies1<br>
-> OrderPacket replies2<br>
-> OrderPacket (replies1 :++: replies2)<br>
(bound at src/Test.lhs:76:3)<br>
In the expression: x :> append xs ys<br>
In an equation for ‘append’:<br>
append (x :> xs) ys = x :> append xs ys<br>
<br>
I suspect I need to adapt the type signature of "append" to suite the<br>
definition.<br>
<br>
Cheers,<br>
<br>
Bas<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div><br></div>