Read/write GADTs as JSON

GADT_JSON.hs

{-# OPTIONS_GHC -fno-warn-type-defaults #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ExtendedDefaultRules #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE RankNTypes #-}

module X where

{-

> let x :: Expr [Int]; x = IfE ((LengthE (ListE [PureE (5 :: Double)]) :: Expr Int) := (PureE 2 :: Expr Int)) (ListE [PureE 1]) (ListE []) in  (encode x)
"{\"tag\":\"IfE\",\"cond\":{\"tag\":\":=\",\"x\":{\"list\":{\"tag\":\"ListE\",\"elements\":[5]},\"tag\":\"LengthE\"},\"y\":2},\"then\":{\"tag\":\"ListE\",\"elements\":[1]},\"else\":{\"tag\":\"ListE\",\"elements\":[]}}"

-}

import Data.Aeson
import Data.Aeson.Types (Parser)
import Data.Text (Text)
import Type.Reflection
import Data.Typeable (cast)

default (Text)

data Expr a where
  IfE :: Typeable a => Expr Bool -> Expr a -> Expr a -> Expr a
  ListE :: Typeable a => [Expr a] -> Expr [a]
  PureE :: OK a => a -> Expr a
  (:=) :: (Eq a, Typeable a) => Expr a -> Expr a -> Expr Bool
  LengthE :: Expr [Double] -> Expr Int

instance (Typeable a, Eq a) => Eq (Expr a) where
  x == y = toJSON x == toJSON y

class (ToJSON a, Typeable a) => OK a
instance OK Int
instance OK Double
instance OK Bool
instance OK a => OK (Expr a)

instance Typeable a => ToJSON (Expr a) where
  toJSON =
    \case
      LengthE expr -> object ["tag" .= "LengthE", "list" .= toJSON expr]
      x := y -> object ["tag" .= ":=", "x" .= x, "y" .= y]
      PureE e -> toJSON e
      IfE cond then' else' ->
        object
          ["tag" .= "IfE", "cond" .= cond, "then" .= then', "else" .= else']
      ListE (exprs :: [Expr exprs]) ->
        object ["tag" .= "ListE", "elements" .= exprs]

instance (Typeable a) => FromJSON (Expr a) where
   parseJSON j =
     case typeRep @a of
      App listish (element :: TypeRep element)
        | Just (HRefl :: list :~~: []) <- eqTypeRep listish (typeRep @[]) ->
           withTypeable element (listParser element j)
      rep |
       Just (HRefl :: list :~~: Int) <- eqTypeRep rep (typeRep @Int) ->
        fmap PureE (parseJSON j)
      rep |
       Just (HRefl :: list :~~: Double) <- eqTypeRep rep (typeRep @Double) ->
        fmap PureE (parseJSON j)
      rep |
       Just (HRefl :: list :~~: Bool) <- eqTypeRep rep (typeRep @Bool) ->
        fmap PureE (parseJSON j)
      _ -> objectParser j

listParser ::
     forall element. Typeable element
  => TypeRep element
  -> Value
  -> Parser (Expr [element])
listParser element j = do
  o <- parseJSON j
  tag <- o .: "tag"
  case tag :: Text of
    "ListE" ->
      withTypeable
        element
        (do array <- o .: "elements" :: Parser [Value]
            values <- mapM (parseJSON :: Value -> Parser (Expr element)) array
            pure (ListE values))
    _ -> objectParser j

objectParser ::
     forall element. Typeable element
  => Value
  -> Parser (Expr element)
objectParser j = do
  o <- parseJSON j
  tag <- o .: "tag"
  case tag :: Text of
    "IfE" -> do
      cond <- o .: "cond"
      then' <- o .: "then"
      else' <- o .: "else"
      pure (IfE cond then' else')
    ":=" -> do
      x <- o .: "x"
      y <- o .: "y"
      case cast (x := y) of
        Just element -> pure element
        Nothing -> fail "expected Bool"
    "LengthE" -> do
      list <- o .: "list"
      case cast (LengthE list) of
        Just element -> pure element
        Nothing -> fail "expected Bool"
    _ -> fail "Invalid tag."