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

[Bas van Dijk]

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 <vogt.adam at gmail.com> 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 <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
>
>