Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Code for Fun with phantom types
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Main where
import Data.Char (ord, chr)
import Text.PrettyPrint.ANSI.Leijen hiding (pretty)
import qualified Data.Ord as DO (compare)
import Prelude hiding (compare)
import Control.Monad (liftM, liftM2)
-- Section 2
data Type a where
RInt :: Type Int
RChar :: Type Char
RList :: Type a -> Type [a]
RPair :: Type a -> Type b -> Type (a, b)
RDyn :: Type Dynamic
RFun :: Type a -> Type b -> Type (a -> b)
RPerson :: Type Person
rString :: Type String
rString = RList RChar
type Bit = Int
toBinary :: Int -> [Bit]
toBinary 0 = []
toBinary x = (x `mod` 2) : (toBinary $ x `div` 2)
toNumber' :: [Bit] -> Int -> Int
toNumber' [] _ = 0
toNumber' (b : bs) t = b * t + toNumber' bs (t * 2)
toNumber :: [Bit] -> Int
toNumber = flip toNumber' 1
padding :: Int -> Int -> [Bit]
padding p x = let b = toBinary x
len = length b
in if p <= len then b
else b ++ take (p - len) (repeat 0)
compressInt :: Int -> [Bit]
compressInt = padding 32
compressChar :: Char -> [Bit]
compressChar x = padding 7 $ ord x
compress :: Type a -> a -> [Bit]
compress RInt x = compressInt x
compress RChar c = compressChar c
compress (RList _) [] = 0:[]
compress (RList ra) (x : xs) = 1 : compress ra x ++ compress (RList ra) xs
compress (RPair ra rb) (x, y) = compress ra x ++ compress rb y
compress RDyn (Dyn ra x) = compressRep (Rep ra) ++ compress ra x
pretty :: Type a -> a -> Doc
pretty RInt i = int i
pretty RChar c = char c
pretty (RList RChar) s = text s
pretty (RList _) [] = text "[]"
pretty (RList ra) (x : xs) = block 1 (text "[" <> pretty ra x <> prettyEnd xs)
where prettyEnd [] = text "]"
prettyEnd (x' : xs') = text "," <> line <> pretty ra x' <> prettyEnd xs'
pretty (RPair ra rb) (x, y) = block 1 (text "(" <> pretty ra x <> text "," <> line <> pretty rb y <> text ")")
pretty RDyn (Dyn ra x) = pretty ra x
block :: Int -> Doc -> Doc
block i d = group (nest i d)
---- Exercise 3
eq :: Type a -> a -> a -> Bool
eq RInt x y = x == y
eq RChar x y = x == y
eq (RList _) [] [] = True
eq (RList ra) (x : xs) (y : ys) | eq ra x y = eq (RList ra) xs ys
| otherwise = False
eq (RList _) _ _ = False
eq (RPair ra rb) (x, y) (x', y') = eq ra x x' && eq rb y y'
eq RDyn (Dyn ra x) (Dyn rb y) = case teq ra rb of
Nothing -> False
Just f -> eq rb (f x) y
compare :: Type a -> a -> a -> Ordering
compare RInt x y = DO.compare x y
compare RChar x y = DO.compare x y
compare (RList _) [] [] = EQ
compare (RList _) [] (_ : _) = LT
compare (RList _) (_ : _) [] = GT
compare (RList ra) (x : xs) (y : ys) = if result == EQ then compare (RList ra) xs ys
else result
where result = compare ra x y
compare (RPair ra rb) (x, y) (x', y') = if first == EQ then compare rb y y' else first
where first = compare ra x x'
compare RDyn (Dyn ra x) (Dyn rb y) = case teq ra rb of
Nothing -> error "cannot compare"
Just f -> compare rb (f x) y
---- Exercise 5
cut :: Int -> [a] -> [[a]]
cut n xs | n >= len = [xs]
| otherwise = left : (cut n right)
where len = length xs
(left, right) = splitAt n xs
-- not finished because of the issue of encoding
uncompress :: Type a -> [Bit] -> a
uncompress RInt i = toNumber i
uncompress RChar c = chr . toNumber $ c
uncompress (RList _) [0] = []
uncompress (RList ra) (_ : xs) = case ra of
RInt -> map toNumber $ cut 32 xs
RChar -> map (chr . toNumber) $ cut 7 xs
-- Section 3
data Dynamic = forall a . Dyn (Type a) a
teq :: Type t -> Type u -> Maybe (t -> u)
teq RInt RInt = return id
teq RChar RChar = return id
teq (RList ra) (RList rb) = liftM map (teq ra rb)
teq (RPair ra1 rb1) (RPair ra2 rb2) = liftM2 (\fa fb (x, y) -> (fa x, fb y)) (teq ra1 ra2) (teq rb1 rb2)
teq (RFun ra1 rb1) (RFun ra2 rb2) = liftM2 (\ f1 f2 f3 -> f2 . f3 . f1) (teq ra2 ra1) (teq rb1 rb2) -- Exercise 9
teq _ _ = fail "cannot teq"
cast :: Dynamic -> Type a -> Maybe a
cast (Dyn ra x) rb = fmap (\f -> f x) (teq ra rb)
---- Exercise 6
data Rep = forall a . Rep (Type a)
compressRep :: Rep -> [Bit]
compressRep (Rep RInt) = [0, 0, 0]
compressRep (Rep RChar) = [0, 0, 1]
compressRep (Rep (RList ra)) = 0:1:0:compressRep (Rep ra)
compressRep (Rep (RPair ra rb)) = 0:1:1:(compressRep (Rep ra) ++ compressRep (Rep rb))
compressRep (Rep RDyn) = [1, 0, 0]
-- Section 4
type Name = String
type Age = Int
data Person = Person Name Age deriving Show
type Traversal = forall a . Type a -> a -> a
tick :: Name -> Traversal
tick s RPerson (Person n a) | s == n = Person n (a + 1)
tick _ _ x = x
copy :: Traversal
copy _ = id
(<.>) :: Traversal -> Traversal -> Traversal
(f <.> g) ra = f ra . g ra
imap :: Traversal -> Traversal
imap f RInt i = i
imap f RChar c = c
imap f (RList ra) [] = []
imap f (RList ra) (x : xs) = f ra x : f (RList ra) xs
imap f (RPair ra rb) (x, y) = (f ra x, f rb y)
imap f RPerson (Person n a) = Person (f rString n) (f RInt a)
everywhere, everywhere' :: Traversal -> Traversal
everywhere f = f <.> imap (everywhere f)
everywhere' f = imap (everywhere' f) <.> f
type Query x = forall a . Type a -> a -> x
isum :: Query Int -> Query Int
isum f RInt a = 0
isum f RChar a = 0
isum f (RList _) [] = 0
isum f (RList ra) (x : xs) = f ra x + f (RList ra) xs
isum f (RPair ra rb) (x, y) = f ra x + f rb y
isum f RPerson (Person n a) = f rString n + f RInt a
total :: Query Int -> Query Int
total f ra t = f ra t + isum (total f) ra t
age :: Type a -> a -> Age
age RPerson (Person _ a) = a
age _ _ = 0
---- Exercise 11
icrush, everything :: (x -> x -> x) -> x -> Query x -> Query x
icrush _ v _ RInt _ = v
icrush _ v _ RChar _ = v
icrush _ v _ (RList _) [] = v
icrush f _ q (RList ra) (x : xs) = f (q ra x) (q (RList ra) xs)
icrush f _ q (RPair ra rb) (x, y) = f (q ra x) (q rb y)
icrush f _ q RPerson (Person n a) = f (q rString n) (q RInt a)
everything f v q ra x = f (q ra x) (icrush f v (everything f v q) ra x)
-- Section 5
infixr :->
data Ty t where
RBase :: Ty Base
(:->) :: Ty a -> Ty b -> Ty (a -> b)
data Term t where
App :: Term (a -> b) -> Term a -> Term b
Fun :: (Term a -> Term b) -> Term (a -> b)
Var :: String -> Term a
vars :: [String]
vars = [c : n | n <- "" : map show [1..], c <- ['a' .. 'z']]
instance Show (Term t) where -- Exercise 12
show x = show (show' x 0)
where
show' :: Term t -> Int -> Doc
show' (App t1 t2) i = text "App" <+> autoParen t1 (show' t1 i) <+> autoParen t2 (show' t2 i)
show' (Fun f) i = text "Fun" <+> parens (text "\\" <> show' (Var (vars !! i)) i <+> text "->" <+> show' (f (Var (vars !! i))) (i + 1))
show' (Var x) _ = text x
autoParen :: Term t -> Doc -> Doc
autoParen (Var _) d = d
autoParen _ d = parens d
newtype Base = In {out :: Term Base}
reify :: Ty a -> a -> Term a
reify RBase v = out v
reify (ra :-> rb) v = Fun (\x -> reify rb (v (reflect ra x)))
reflect :: Ty a -> Term a -> a
reflect RBase e = In e
reflect (ra :-> rb) e = \x -> reflect rb (App e (reify ra x))
test = reify ((b :-> b) :-> b :-> b) (t2 (t2 t3))
where t1 = s (k s)
t2 = s (t1 (s (k k) i))
t3 = k i
s = \ x y z -> (x z) (y z)
k = \ x _ -> x
i = \ x -> x
b :: Ty Base
b = RBase
-- Section 6
data Dir x y where
Lit :: String -> Dir x x
Int :: Dir x (Int -> x)
String :: Dir x (String -> x)
(:^:) :: Dir y1 y2 -> Dir x y1 -> Dir x y2
format' :: Dir x y -> (String -> x) -> (String -> y)
format' (Lit s) = \c out -> c (out ++ s)
format' Int = \c out -> \i -> c (out ++ show i)
format' String = \c out -> \s -> c (out ++ s)
format' (d1 :^: d2) = \c out -> format' d1 (format' d2 c) out
format :: Dir String y -> y
format d = format' d id ""
---- Exercise 15
data DirL a where
LEnd :: DirL String
LLit :: String -> DirL a -> DirL a
LInt :: DirL a -> DirL (Int -> a)
LString :: DirL a -> DirL (String -> a)
formatL' :: DirL a -> String -> a
formatL' LEnd c = c
formatL' (LLit s d) c = formatL' d (c ++ s)
formatL' (LInt d) c = \i -> formatL' d (c ++ show i)
formatL' (LString d) c = \s -> formatL' d (c ++ s)
formatL :: DirL a -> a
formatL = flip formatL' ""
-- Section 7
newtype a :=: b = Proof {apply :: forall f . f a -> f b}
refl :: a :=: a
refl = Proof id
newtype Flip f a b = Flip {unFlip :: f b a}
symm :: (a :=: b) -> (b :=: a)
symm p = unFlip (apply p (Flip refl))
trans :: (a :=: b) -> (b :=: c) -> (a :=: c)
trans p q = Proof (apply q . apply p)
---- Exercise 17
newtype Func a b = Func {unFunc :: a -> b}
newtype Func' a b = Func' {unFunc' :: b -> a}
from :: (a :=: b) -> (a -> b)
from p = unFunc (apply p (Func id))
to :: (a :=: b) -> (b -> a)
to p = unFunc' (apply p (Func' id))
-- Dummy main
main :: IO ()
main = putStrLn "Code for Fun with phantom types. See the source."
-- http://www.cs.ox.ac.uk/ralf.hinze/publications/With.pdf
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment