How to differentiate GADT constructors with different phantom types?

Question

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

It might be helpful to include the required language features for people trying to run it themselves (GADTs, DataKinds, RankNTypes, KindSignatures) — Aplet123
Your functions fall afoul of Parse, don't validate. You should consider adding data SomeRequest where SomeRequest :: forall f. Message f Request -> SomeRequest, and changing your functions' types to filterToRequests :: [SomeMessage] -> [SomeRequest] and filterToClientRequests :: [SomeMessage] -> [Message FromClient Request]. — Joseph Sible-Reinstate Monica
@JosephSible-ReinstateMonica I wish I could, see my follow-up comment on the answer :) — tom

shayan shayan · Accepted Answer · 2020-12-16T03:00:19

My solution utilizes the fact that GADT constructors expose any existential type constraints in their scope upon pattern matching. The trick was to introduce two type classes KnownSender and KnownType that allow to convert their respective kind variables to runtime values:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

data From = FromClient | FromServer deriving (Eq)
data MessageType = Request | Notification deriving (Eq)

data Message (from :: From) (typ :: MessageType) where
  Request1 :: Message 'FromClient 'Request
  Request2 :: Message 'FromClient 'Request
  Request3 :: Message 'FromServer 'Request
  Notification1 :: Message 'FromClient 'Notification

data SomeMessage where
  SomeMessage :: forall f t. KnownTags f t => Message f t -> SomeMessage

class KnownSender (f :: From) where
  knownSenderVal :: From

instance KnownSender 'FromClient where
  knownSenderVal = FromClient
instance KnownSender 'FromServer where
  knownSenderVal = FromServer
    
class KnownType (t :: MessageType) where
  knownTypeVal :: MessageType

instance KnownType 'Request where
  knownTypeVal = Request
instance KnownType 'Notification where
  knownTypeVal = Notification

type KnownTags f t = (KnownSender f, KnownType t)

knownTags :: SomeMessage -> (From,MessageType)
knownTags (SomeMessage msg) = knownTags' msg -- Magic happens here!
  where
    -- This function may also be written at the top level should you need it.
    knownTags' :: forall f t . KnownTags f t => Message f t -> (From, MessageType)
    knownTags' _ = (knownSenderVal @f ,knownTypeVal @t)

allMessages = [SomeMessage Request1
              , SomeMessage Request2
              , SomeMessage Request3
              , SomeMessage Notification1]

-- Desired output: [SomeMessage Request1, SomeMessage Request2, SomeMessage Request3]
filterToRequests :: [SomeMessage] -> [SomeMessage]
filterToRequests = filter ((== Request) . snd . knownTags)
-- Desired output: [SomeMessage Request1, SomeMessage Request2]
filterToClientRequests :: [SomeMessage] -> [SomeMessage]
filterToClientRequests = filter ((== FromClient) . fst . knownTags)

Take note that your SomeMessage type had to be slightly modified to include the KnownTags constraint in its constructor. the Eq instances for both From and MessageType were also added.

Update:

As per your comment, if you need to have a [SomeMessage] -> [SomeRequestMessage] function, one way is to use reflection:

{-# LANGUAGE FlexibleContexts #-}

import Type.Reflection (TypeRep,Typeable,typeRep,eqTypeRep)
import Data.Type.Equality
import Data.Maybe (maybeToList)

-- Add Typeable constraints for f and t
type KnownTags f t = (Typeable f,KnownSender f, Typeable t, KnownType t)

-- General utility function useful for dynamic programming and reflection
withKnownMsg :: forall a . SomeMessage -> (forall f t . KnownTags f t => Message f t -> a) -> a
withKnownMsg (SomeMessage msg) f = f msg

data SomeRequestMessage where
  SomeRequestMessage :: forall f. KnownTags f 'Request => Message f 'Request -> SomeRequestMessage

toSomeRequest :: SomeMessage -> Maybe SomeRequestMessage
toSomeRequest someMsg = withKnownMsg someMsg f
  where
    f :: forall f t . (KnownTags f t) => Message f t -> Maybe SomeRequestMessage
    f msg = fmap (\HRefl -> SomeRequestMessage msg). eqTypeRep (typeRep @t) $ typeRep @'Request

someRequestMsgs :: [SomeMessage] -> [SomeRequestMessage]
someRequestMsgs msgs = msgs >>= (maybeToList . toSomeRequest)

How to differentiate GADT constructors with different phantom types?

2 Answers