Last active
March 13, 2018 13:24
-
-
Save cdparks/bc76a12bc76e9f8c8112236880dd2e58 to your computer and use it in GitHub Desktop.
(De)serializing GADTs using an intermediate untyped representation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment