Design - part 2 - Putting types to work

Posted on April 12, 2017

Where we venture into using types as drivers, not just as verifiers.

illustrating ideas from fun with phantom type the commented code is from here

Warmup - Interpreter

If we represent a language with untyped Exp data type, when consuming a represented program, we have to add type coercions to convince the type system : we check the value of type Exp received really contains the expected data inside, and we assert that to the compiler in some way to do something with it.

If we use GADT, some extra type information is packed with the data constructor/destructor. as we pattern math on the value, the type become more precise as the index gets fixed. we uncover type information as we uncover data information.

This makes evaluation straightforward :

data Term1 a where
  Zero :: Term1 Int
  Succ :: Term1 Int -> Term1 Int
  Pred :: Term1 Int -> Term1 Int
  IsZero :: Term1 Int  ->  Term1 Bool
  If :: Term1 Bool -> Term1 a -> Term1 a -> Term1 a

eval :: forall a. Term1 a -> a
eval (Zero {- a is bound to Int from here-})  = 0 -- so 0 :: Int
eval (Succ n{- a is bound to Int from here-}) = eval n {-:: Int -} + 1 -- type correct
eval (Pred n)                                 = eval n - 1
eval (IsZero n)                               = eval n == 0
eval (If e1 e2 e3) = if eval e1 then eval e2 else eval e3

There can not be a function map :: (a -> b) -> Term1 a -> Term1 b

The type index in term does not mean there is a value of that type in it to apply a -> b to. It is called a “phantom type”, other name for an type index seen as a “pure index” a for the overall type Term a, not necessarily linked to a data. The type level has a life on its own. It more accurately reflect static information. the type of some variable, is, in a static language, part of the available information statically, but only a subset of it.

Generic Function

The problem

We want to compress data. We would like the same procedure to works for many types of data, provided its type can be described as a combination of basic types. This description could have been a type level description through with type classes, but here we have a value describing a type a. that value, named representation of a type will be of type Type a.

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

Our goal is to parameterize a function compress with the representation of the type of the value given. Different values yield different types for the resulting curried function

With all this we have access to the following magically safe operations :

> _ = compress RInt :: Int -> [Bit]
> _ = compress (RPair RInt RChar) :: (Int, Char) -> [Bit]

(Having the compiler to find a representation for any types is the subject of a reflection on types see also slides in ghc 8.2)

This is achieved in a similar way that the eval function

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

The correct way to see compress is as a family of functions, indexed by a value representing a type. We could index directly with a type, and get rid of the representation. This then requires type classes. Type class allow to talk about, say, compressable types and require that as an implicit constraint. The compiler would do for you the job of selecting the correct function from this famility with no representation being passed around. Another difference is that this selection would wire the correct function at static time and not require an interpretation at run time resulting in faster code.

Equality, comparison, ..

To see that this is a general concept, we can provide generically other operations which are naturally thought of as generic : if we can compare the parts, we should be able to compare structures made of the parts.

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 = x y
compare RChar x y = 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

Boosting compress

compress has type Type a -> TCompress a where TCompress a = a -> [Bit] This type function works Compare need a value (the representation)

The open world