I'm working on a system (inspired by lsp-types) that uses GADTs tagged with type information to represent the different types of messages exchanged by a client and server:
{-# LANGUAGE GADTs, DataKinds, KindSignatures, RankNTypes #-}
data From = FromClient | FromServer
data MessageType = Request | Notification
data Message (from :: From) (typ :: MessageType) where
Request1 :: Message FromClient Request
Request2 :: Message FromClient Request
Request3 :: Message FromServer Request
Notification1 :: Message FromClient Notification
My question is, given a list of these constructors (in an existential wrapper), how can I select a subset of them that have a certain type?
data SomeMessage where
SomeMessage :: forall f t. Message f t -> SomeMessage
allMessages = [SomeMessage Request1
, SomeMessage Request2
, SomeMessage Request3
, SomeMessage Notification1]
-- Desired output: [SomeMessage Request1, SomeMessage Request2, SomeMessage Request3]
filterToRequests :: [SomeMessage] -> [SomeMessage]
filterToRequests allMessages = undefined
-- Desired output: [SomeMessage Request1, SomeMessage Request2]
filterToClientRequests :: [SomeMessage] -> [SomeMessage]
filterToClientRequests allMessages = undefined