Skip to content

Instantly share code, notes, and snippets.

@cdparks

cdparks/Typed.hs

Last active Mar 13, 2018
Embed
What would you like to do?
(De)serializing GADTs using an intermediate untyped representation
#!/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
You can’t perform that action at this time.