Code for Fun with phantom types

GADT.hs

{-# 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