How to implement prism for GADT?

Question

I have GADT data type like this:

data TValue = TInt | TBool

data Value (t :: TValue) where
    I :: Int  -> Value 'TInt
    B :: Bool -> Value 'TBool

And I want to have prisms for pattern matching on this data type. I'm using data prism approach for simplicity. So previously I had something like this:

data ValuePrism (tag :: TValue) a = ValuePrism
    { matchValue :: forall t . Value t -> Maybe a
    , buildValue :: a -> Value tag
    }

boolPrism :: ValuePrism 'TBool Bool
boolPrism = ValuePrism matchBool B
  where
    matchBool :: Value t -> Maybe Bool
    matchBool (B b) = Just b
    matchBool _     = Nothing

I want to fit this use case into prisms interface. I can specify type in the following way:

data Prism s t a b = Prism
    { preview :: s -> Either t a
    , review  :: b -> t
    }

type ValuePrism (tag :: TValue) a = 
    forall t . Prism (Value t) (Value tag) a a

But I'm unable to write function which creates ValuePrism according to old interface:

mkValuePrism :: (forall t . Value t -> Maybe a)
             -> (a -> Value tag)
             -> ValuePrism tag a
mkValuePrism = =<< (ツ) >>=

Is there some way to create prism for GADT?

Daniel Wagner Daniel Wagner · Accepted Answer · 2018-06-20T14:46:12

You'll need to change your second definition of ValuePrism.

Your first ValuePrism 'TBool Bool does not contain a function of type Bool -> Value 'TInt, but your second ValuePrism 'TBool Bool does (by specializing the forall'd t to 'TInt and calling review). Such a function can be cooked up from scratch, but it will necessarily be what I would call "unreasonable". You could define

type ValuePrism tag a = Prism (Value tag) (Value tag) a a

instead; you will then find the translation much easier.

How to implement prism for GADT?

1 Answers