This Jupyter notebook contains my solutions to some exercises from Fun with Phantom Types by Ralf Hinze.
Original author: David Banas capn.freako@gmail.com
Original date: July 30, 2017
Copied from: norm_by_eval.hs (Original response to Ex. 12, authored on July 9, 2015.)
Copyright © 2017 David Banas; all rights reserved World wide.
In [1]:
import Data.Time
putStrLn "Notebook last run:"
getCurrentTime
Phantom Types is a somewhat, if not exactly, synonymous term to Generalized Algebraic Data Types (GADTs), which is used more frequently now. Ralf uses an older syntax for defining GADTs, which doesn't compile in more recent versions of GHC. (Did it ever?) Here is an example translation from Ralf's syntax to the current syntax:
In [2]:
data Term t = Zero with t = Int
| Succ (Term Int) with t = Int
| Pred (Term Int) with t = Int
| IsZero (Term Int) with t = Bool
| If (Term Bool) (Term a) (Term a) with t = a
In [3]:
{-# LANGUAGE GADTs #-}
data Term t where
Zero :: Term Int
Succ :: Term Int -> Term Int
Pred :: Term Int -> Term Int
IsZero :: Term Int -> Term Bool
If :: Term Bool -> Term a -> Term a -> Term a
Note that Ralf alludes to the new syntax, above, in Ex. 2.
In [4]:
eval :: Term t -> t
eval (Zero) = 0
eval (Succ e) = eval e + 1
eval (Pred e) = eval e - 1
eval (IsZero e) = eval e == 0
eval (If e1 e2 e3) = if eval e1 then eval e2 else eval e3
In [5]:
let one = Succ Zero
:type one
eval one
eval (IsZero one)
IsZero (IsZero one)
In [6]:
eval (If (IsZero one) Zero one)
let true = IsZero Zero
let false = IsZero one
eval (If true true false)
Families of type-indexed functions can be implemented either using type classes or using type representations. Discuss differences and commonalities of the two approaches.
As an alternative to simply answering this question, I'm going to attempt to implement the functionality introduced in this chapter, using type classes.
Note: There's no need to write pretty, in this case, as we can just rely on the exisitng Show instances of the standard types we're using. Likewise for compare.
This prompts one obvious answer to the exercise question: Using type classes obviates the need to write our own utility functions, which we get for free, via the default instances of the standard types.
In [7]:
{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-}
-- module Main where
import Data.Char (ord, chr)
-- Our "bit" representation.
data Bit = O -- 0
| I -- 1
deriving (Show, Eq)
-- Generic conversions from Int to [Bit] and back.
intToBits :: Int -> [Bit]
intToBits n | n < 0 = error "No negative Ints!"
| n == 0 = []
| n `mod` 2 /= 0 = I : msbs
| otherwise = O : msbs
where msbs = intToBits (n `div` 2)
bitsToInt :: [Bit] -> Int
bitsToInt = bitsToInt' 1
bitsToInt' :: Int -> [Bit] -> Int
bitsToInt' _ [] = 0
bitsToInt' w (b:bs) | b == I = w + bitsToInt' w' bs
| otherwise = 0 + bitsToInt' w' bs
where w' = w * 2
-- Typeclass representing compressable data types.
class Compressable t where
-- bitLen :: Int -- Why doesn't this work?
bitLen :: t -> Int
toInt :: t -> Int
fromInt :: Int -> t
-- the "generic" functions
compress :: t -> [Bit]
compress x | neededFill < 0 = error "Value overflow!"
| otherwise = prelimRes ++ (take neededFill (repeat O))
where prelimRes = intToBits $ toInt x
neededFill = bitLen x - length prelimRes
uncompress :: [Bit] -> (t, [Bit]) -- Returns the unconsumed bits.
uncompress bs | length bs < bitLen x = error "Insufficient bits!"
| otherwise = ( x, drop (bitLen x) bs)
where x = fromInt (bitsToInt (take (bitLen x) bs))
instance Compressable Int where
bitLen _ = 32
toInt = id
fromInt = id
instance Compressable Char where
bitLen _ = 7
toInt = ord
fromInt = chr
instance Compressable a => Compressable [a] where
bitLen xs = sum $ map bitLen xs
toInt = undefined
fromInt n = undefined
compress [] = O : []
compress (x:xs) = I : compress x ++ compress xs
uncompress [] = error "Empty list!"
uncompress (b:bs) | b == O = ([] , bs)
| b == I = (head' : tail', unusedBits)
where head' = fst recRes
tail' = fst $ recRes'
unusedBits = snd $ recRes'
recRes = uncompress bs
recRes' = uncompress $ snd recRes
instance (Compressable a, Compressable b) => Compressable (a, b) where
bitLen (x, y) = bitLen x + bitLen y
toInt = undefined
fromInt = undefined
compress (x, y) = compress x ++ compress y
uncompress bs = let (x, bs') = uncompress bs
(y, bs'') = uncompress bs'
in ((x, y), bs'')
main :: IO ()
main = do
let x = compress (5 :: Int)
print x
let y = compress ('A' :: Char)
print y
let z = compress ['A', 'B']
print z
print $ compress ('A', 5 :: Int)
print $ compress 'A' == compress 'A'
print $ compress 'A' == compress 'B'
print $ ((uncompress x) :: (Int, [Bit]))
print $ ((uncompress y) :: (Char, [Bit]))
print $ ((uncompress z) :: ([Char], [Bit]))
main
In [8]:
{-# LANGUAGE ExplicitForAll #-}
import Control.Monad.State
newtype Base = In{out :: Term Base}
infixr :->
data Type t where
RBase :: Type Base
(:->) :: Type a -> Type b -> Type (a -> b)
b :: Type Base
b = RBase
data Term t where
App :: Term (a -> b) -> Term a -> Term b
Fun :: (Term a -> Term b) -> Term (a -> b)
Var :: String -> Term t
reify :: forall t. Type t -> t -> Term t
reify RBase v = out v
reify (ra :-> rb) v = Fun (reify rb . v . reflect ra)
reflect :: forall t. Type t -> Term t -> t
reflect RBase expr = In expr
reflect (ra :-> rb) expr = reflect rb . App expr . reify ra
-- Exercise 12 - Implement show() for 'Term t'.
allNames :: [String]
allNames = map reverse $ tail allNames' where
allNames' = "" : [suf : base | base <- allNames', suf <- ['a'..'z']]
instance Show (Term t) where
show x = evalState (showTerm x) allNames
showTerm :: Term t -> State [String] String
showTerm (Var str) = return str
showTerm (App f (Var str)) = do
fStr <- showTerm f
return $ "App " ++ fStr ++ " " ++ str
showTerm (App f x) = do
fStr <- showTerm f
xStr <- showTerm x
return $ "App " ++ fStr ++ " (" ++ xStr ++ ")"
showTerm (Fun rf) = do
varNames <- get
let varName = head varNames
put $ tail varNames
rfStr <- showTerm (rf (Var varName))
return $ "Fun (\x3BB" ++ varName ++ " -> " ++ rfStr ++ ")"
-- Hinze's interactive testing repeated, here.
s :: forall t t1 t2. (t2 -> t1 -> t) -> (t2 -> t1) -> t2 -> t
s x y z = x z (y z)
k :: forall t t1. t1 -> t -> t1
k x _ = x
i :: forall t. t -> t
i x = x
e =s (s (k s) (s (k k) i))((s ((s (k s))((s (k k))i)))(k i))
print $ reify (b :-> b) (s k k)
print $ reify (b :-> (b :-> b)) (s (k k)i)
print $ reify ((b :-> b) :-> (b :-> b)) e
In [ ]: