How to construct values from multiple GADTs while parsing json?

Question

I have the following data structures:

data Operator :: * -> * where
  StringEquals     :: Operator String
  StringNotEquals  :: Operator String
  NumericEquals    :: Operator Integer
  NumericNotEquals :: Operator Integer

data Variable :: * -> * where
  UserName     :: Variable String
  RequestPath  :: Variable String
  BodyLength   :: Variable Integer

data Value :: * -> * where
  StringValue     :: String -> Value String
  NumericValue    :: Integer -> Value Integer

data Condition a = Condition (Operator a) (Variable a) (Value a)

that will be used in functions like these:

extractVariable :: Variable a -> HttpRequest -> a
evaluate :: Operator a -> Value a -> a -> Bool

I'd like to parse Conditions from a JSON file. I can parse the parts individually, wrapped with Some, but not sure how to construct a Condition from them. The following works and shows what I'd like to do, but it obviously isn't scalable to write:

import Data.Some

parseCondition :: Some Operator -> Some Variable -> Some Value -> Parser (Some Condition)
parseCondition (Some op@StringEquals) (Some var@UserName) (Some val@(StringValue _)) = return $ mkSome $ Condition op var val
parseCondition (Some op@StringNotEquals) (Some var@UserName) (Some val@(StringValue _)) = return $ mkSome $ Condition op var val
parseCondition (Some op@StringEquals) (Some var@RequestPath) (Some val@(StringValue _)) = return $ mkSome $ Condition op var val
parseCondition (Some op@StringNotEquals) (Some var@RequestPath) (Some val@(StringValue _)) = return $ mkSome $ Condition op var val
parseCondition (Some op@NumericEquals) (Some var@BodyLength) (Some val@(NumericValue _)) = return $ mkSome $ Condition op var val
parseCondition _ _ _ = parseFail "incompatible types"

What's the best way to do this in haskell?

user_5684257 · Answer

Given a Operator a (resp. Variable a, Value a) you know exactly what a is. Using that the standard type that represents complete knowledge of a type a is TypeRep a, express that knowledge in code.

import Type.Reflection -- NOT the other TypeRep

operatorType :: Operator a -> TypeRep a
operatorType StringEquals = typeRep
operatorType StringNotEquals = typeRep
operatorType NumericEquals = typeRep
operatorType NumericNotEquals = typeRep

variableType :: Variable a -> TypeRep a
variableType UserName = typeRep
variableType RequestPath = typeRep
variableType BodyLength = typeRep

valueType :: Value a -> TypeRep a
valueType (StringValue _) = typeRep
valueType (NumericValue _) = typeRep

That is a lot of boilerplate, but the idea is that it now scales as one line per constructor rather than one line per possible combination of three constructors. Also, it looks like it can be automated, though I don't know of any "premade" solution for that.

Now just use the equality test on TypeReps.

import Data.Type.Equality
-- data a :~: b where Refl :: a :~: a
-- testEquality :: TypeRep a -> TypeRep b -> Maybe (a :~: b)

-- data Some f = forall a. Some (f a) -- I guess?
makeCondition :: Some Operator -> Some Variable -> Some Value -> Maybe (Some Condition)
makeCondition (Some op) (Some v) (Some x) = do -- I generally prefer guards for this "proofwork" but in this case a do happens to work
  Refl <- operatorType op `testEquality` variableType v
  Refl <- variableType v `testEquality` valueType x
  return $ Some $ Condition op v x

How to construct values from multiple GADTs while parsing json?

1 Answers