(De)serializing GADTs using an intermediate untyped representation

Typed.hs

#!/usr/bin/env stack
-- stack --resolver lts-10.8 script

-- Serializing and deserializing GADTs by using an intermediate
-- untyped representation.
--
-- Typed     | List [And (Not (Equals (Int 1) (Int 2))) (Equals (Bool True) (Bool False)),Bool False]
-- Annotated | List [And (Not (Equals (Int 1) (Int 2))) (Equals (Bool True) (Bool False)),Bool False] ::: ListTy BoolTy
-- Erased    | UList [UAnd (UNot (UEquals (UInt 1) (UInt 2))) (UEquals (UBool True) (UBool False)),UBool False]
-- Encoded   | "{\"List\":[{\"And\":[{\"Not\":{\"Equals\":[{\"Int\":1},{\"Int\":2}]}},{\"Equals\":[{\"Bool\":true},{\"Bool\":false}]}]},{\"Bool\":false}]}"
-- Decoded   | Just (List [And (Not (Equals (Int 1) (Int 2))) (Equals (Bool True) (Bool False)),Bool False] ::: ListTy BoolTy)
--
-- See http://augustss.blogspot.ie/2009/06/more-llvm-recently-someone-asked-me-on.html

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}

module Typed where

import Control.Applicative
import Control.Monad
import Data.Aeson hiding (Bool)
import Data.Aeson.Types hiding (Bool)
import qualified Data.ByteString.Lazy as LBS
import qualified Data.HashMap.Strict as HashMap
import Data.Traversable

data Untyped where
  UInt :: Int -> Untyped
  UBool :: Bool -> Untyped
  UIf :: Untyped -> Untyped -> Untyped -> Untyped
  UAnd :: Untyped -> Untyped -> Untyped
  UOr :: Untyped -> Untyped -> Untyped
  UEquals :: Untyped -> Untyped -> Untyped
  UNot :: Untyped -> Untyped
  UList :: [Untyped] -> Untyped

deriving instance Show Untyped

data Val a where
  Int :: Int -> Val Int
  Bool :: Bool -> Val Bool
  If :: Val Bool -> Val a -> Val a -> Val a
  And :: Val Bool -> Val Bool -> Val Bool
  Or :: Val Bool -> Val Bool -> Val Bool
  Equals :: Val a -> Val a -> Val Bool
  Not :: Val Bool -> Val Bool
  List :: [Val a] -> Val [a]

deriving instance Show (Val a)

instance FromJSON Untyped where
  parseJSON (Object o) =
    case HashMap.toList o of
      [] -> fail "Empty object as val"
      [("If", o')] -> do
        (cond, t, f) <- parseJSON o'
        pure $ UIf cond t f
      [("And", o')] -> do
        (x, y) <- parseJSON o'
        pure $ UAnd x y
      [("Equals", o')] -> do
        (x, y) <- parseJSON o'
        pure $ UEquals x y
      [("Or", o')] -> do
        (x, y) <- parseJSON o'
        pure $ UOr x y
      [("Not", o')] -> do
        x <- parseJSON o'
        pure $ UNot x
      [("Bool", o')] -> do
        x <- parseJSON o'
        pure $ UBool x
      [("Int", o')] -> do
        x <- parseJSON o'
        pure $ UInt x
      [("List", o')] -> do
        xs <- parseJSON o'
        pure $ UList xs
  parseJSON _ = fail "Expected object"

instance ToJSON Untyped where
  toJSON = \case
    UInt i ->
      object ["Int" .= i]
    UBool b ->
      object ["Bool" .= b]
    UIf cont t f ->
      object ["If" .= (cont, t, f)]
    UAnd x y ->
      object ["And" .= (x, y)]
    UOr x y ->
      object ["Or" .= (x, y)]
    UEquals x y ->
      object ["Equals" .= (x, y)]
    UNot x ->
      object ["Not" .= x]
    UList xs ->
      object ["List" .= xs]

-- Term level types
data Type a where
  BoolTy :: Type Bool
  IntTy :: Type Int
  ListTy :: Type a -> Type [a]

deriving instance Show (Type a)

-- Read ":::" as a term-level "has-type"
-- e.g.
--   Int 3 ::: IntTy
-- is the same as
--   3 has type Int
infix 2 :::
data Typed = forall a. Val a ::: Type a

deriving instance Show Typed

-- Term-level witness for type-level equality
data EqTy a b where
  EqTy :: EqTy a a

deriving instance Show (EqTy a b)

eqTy :: MonadPlus m => Type a -> Type b -> m (EqTy a b)
eqTy BoolTy BoolTy = pure EqTy
eqTy IntTy IntTy = pure EqTy
eqTy (ListTy xTy) (ListTy yTy) = do
  EqTy <- eqTy xTy yTy
  pure EqTy
eqTy _ _ = mzero

typecheck :: MonadPlus m => Untyped -> m Typed
typecheck = \case
  UInt i ->
    pure $ Int i ::: IntTy
  UBool b ->
    pure $ Bool b ::: BoolTy
  UIf ucond ut uf -> do
    cond ::: BoolTy <- typecheck ucond
    t ::: tTy <- typecheck ut
    f ::: fTy <- typecheck uf
    EqTy <- eqTy tTy fTy
    pure $ If cond t f ::: tTy
  UAnd ux uy -> do
    x ::: BoolTy <- typecheck ux
    y ::: BoolTy <- typecheck uy
    pure $ And x y ::: BoolTy
  UOr ux uy -> do
    x ::: BoolTy <- typecheck ux
    y ::: BoolTy <- typecheck uy
    pure $ Or x y ::: BoolTy
  UEquals ux uy -> do
    x ::: xTy <- typecheck ux
    y ::: yTy <- typecheck uy
    EqTy <- eqTy xTy yTy
    pure $ Equals x y ::: BoolTy
  UNot ux -> do
    x ::: BoolTy <- typecheck ux
    pure $ Not x ::: BoolTy
  UList [] -> mzero
  UList (ux:uxs) -> do
    x ::: xTy <- typecheck ux
    xs <- for uxs $ \uy -> do
      y ::: yTy <- typecheck uy
      EqTy <- eqTy xTy yTy
      pure y
    pure $ List (x:xs) ::: ListTy xTy

erase :: Typed -> Untyped
erase (typed ::: _) = go typed
 where
  go :: forall a. Val a -> Untyped
  go = \case
    Int i ->
      UInt i
    Bool b ->
      UBool b
    If cond t f ->
      UIf (go cond) (go t) (go f)
    And x y ->
      UAnd (go x) (go y)
    Or x y ->
      UOr (go x) (go y)
    Equals x y ->
      UEquals (go x) (go y)
    Not x ->
      UNot (go x)
    List xs ->
      UList (map go xs)

decodeTyped :: LBS.ByteString -> Maybe Typed
decodeTyped = typecheck <=< decode

encodeTyped :: Typed -> LBS.ByteString
encodeTyped = encode . erase

main :: IO ()
main = do
  putStrLn $ "Typed     | " ++ show typed
  putStrLn $ "Annotated | " ++ show annotated
  putStrLn $ "Erased    | " ++ show erased
  putStrLn $ "Encoded   | " ++ show encoded
  putStrLn $ "Decoded   | " ++ show decoded
 where
  typed =
    List
    [ And
        (Not (Equals (Int 1) (Int 2)))
        (Equals (Bool True) (Bool False))
    , Bool False
    ]
  annotated = typed ::: ListTy BoolTy
  erased = erase annotated
  encoded = encodeTyped annotated
  decoded = decodeTyped encoded