Code and Notes (Week 7 Thursday)

This is the Haskell demo code I showed during the lecture. Many thanks to Craig McLaughlin for the original.

Below that, I've presented an additional exercise (and solution) for constructing a typing derivation tree for an expression including unroll that we completed only partially during the lecture.

Reminders:

ghc Main will compile Main.hs to an executable binary.
ghci will open a read-eval-print loop (REPL).
- There, use :l Main.hs to compile and load Main.hs.
- After that you can invoke individual functions of Main directly.

-- Week 7B: Algebraic Data Types in Haskell
{-# LANGUAGE EmptyCase #-}
module Main where

-- Product type definition
data Product a b = MkProd a b

-- Haskell's built-in product type uses "tuple" syntax
-- :: (a × b) on the slides
myProd :: (Int, Bool)
myProd = (1, False)

-- Sum type definition
data Sum a b = Inl a | Inr b

myOtherSumL :: Sum Int Bool
myOtherSumL = Inl 1

-- Haskell's built-in sum type is "Either"
-- :: (a + b) on the slides
mySumL :: Either Int Bool
mySumL = Left 1

mySumR :: Either Int Bool
mySumR = Right True

-- Unit type definition
data Unit = Unit

-- Haskell's built-in unit type is () with unit value ()
-- :: 1 on the slides
-- () :: ()
myUnit :: ()
myUnit = ()

-- Empty type definition
-- (NB: The {-# LANGUAGE EmptyCase #-} at the top of the file
-- may be needed to allow us to declare this.)
data Void

-- Haskell's standard library empty type is Data.Void
-- (you can import it)
-- import Data.Void

-- Empty type eliminator: No cases!
-- :: 0 -> a on the slides
absurd :: Void -> a
absurd x = case x of {}

-- Type corresponding to negation in constructive logics
type Not a = a -> Void

-- Functions corresponding to proofs in constructive logics
-- Here, x :: a, and f :: a -> Void, so it's implementable.
two :: a -> Not (Not a)
-- :: a -> ((a -> Void) -> Void)
two x f = f x
-- Note, it's double negation elimination,
--   i.e. Not (Not a) -> a,
-- that doesn't have a constructive proof. To see why,
-- try defining a terminating function of this type!
-- :: ((a -> Void) -> Void) -> a

contra :: (a -> b) -> (Not b -> Not a)
contra f g = g . f

dist_or :: Not (Sum a b) -> ((Not a), (Not b))
dist_or f = (\a -> f (Inl a), \b -> f (Inr b))
-- Note, the backslash \ above is a lambda in Haskell.
-- \_ -> blah corresponds to λ_. blah

-- Some non-terminating functions that are well typed in Haskell
spin :: Int -> Bool
spin = spin

-- These two, if interpreted as proofs, contradict each other:
proof1 :: (Int -> Bool, Bool -> Int) -- Int = Bool ?
proof1 = proof1

proof2 :: Not (Int -> Bool, Bool -> Int) -- Int != Bool ?
proof2 = proof2

-- The list defined in the slides was only for Ints.
-- data IntList = Nil | Cons Int IntList

-- But Haskell supports polymorphic types.
-- Note here the polymorphism of type MyList over
-- type variable a - more info on that in Week 8.
data MyList a = MyNil | MyCons a (MyList a)

-- Here's an example of a recursive type
data BinTree = Leaf | Node BinTree BinTree
-- Its type will use form: rec t . T
-- Using the procedure from the lecture slides
-- we can rewrite it roughly as follows:
-- Leaf | Node BinTree BinTree
-- ~> 1 + 1 × (BinTree × BinTree)
-- ~> rec t. 1 + 1 × (t × t)
-- ~> rec t. 1 + (t × t)

-- Type checking a recursive type

-- Example 1: Leaf
myLeaf :: BinTree
myLeaf = Leaf
-- Leaf ~ roll (Inl ())
--
-- Typing derivation tree:
--
-- (Inl ()) :: 1 + a
-- (Inl ()) ::
--   1 + ((rec t. 1 + (t × t)) × (rec t. 1 + (t × t)))
-- ---------------------------------------------------
--          roll (Inl ()) :: rec t. 1 + (t × t)

-- Example 2: Node Leaf Leaf
myNode :: BinTree
myNode = Node Leaf Leaf
--
-- Typing derivation tree:
--
-- (see Example 1 above for the rest)
-- -----------------------------------
-- roll (Inl ()) :: rec t. 1 + (t × t) <- same hypothesis
-- -----------------------------------    for fst and snd
-- (roll (Inl ()), (Inl ())) ::
--   (rec t. 1 + (t × t)) × (rec t. 1 + (t × t))
-- ---------------------------------------------------
-- Inr (roll (Inl ()), roll (Inl ())) ::
--   1 + ((rec t. 1 + (t × t)) × (rec t. 1 + (t × t)))
-- ---------------------------------------------------
-- roll Inr (roll (Inl ()), roll (Inl ())) ::
--   rec t. 1 + (t × t)

describeT :: (String, Integer) -> String
describeT (s, n) =
  "humans say: " ++ (show s) ++ "\n" ++
  "de Bruijn says: " ++ (show n)

-- For completeness, so the module can be compiled
main :: IO ()
main = putStrLn $ describeT ("x",0)

At the end of the lecture, we started to construct a typing derivation tree for unroll [1, 2], which without the syntactic sugar should be unroll [1,2] = unroll (roll (InR (1, roll (InR (2, roll (InL ())))))).

First, we reasoned that one step of the dynamic semantics (unroll cancelling roll) should take us to InR (1, roll (InR (2, roll (InL ())))), and started deriving the type for that as follows (leaving out the typing environments Gamma, which don't happen to change for any of the rules we've used yet below):

                              TODO1
                -----------------------------------
1 :: Int        roll (InR (2, roll (InL ()))) :: t4
---------------------------------------------------
(1, roll (InR (2, roll (InL ())))) :: Int × t4
---------------------------------------------------------
InR (1, roll (InR (2, roll (InL ())))) :: t1 + (Int × t4)

We got as far as the TODO1 above, which would need to be completed to figure out what the unknown type variables t1 and t4 are.

Next, we started deriving the type for the original expression including the initial unroll (roll ...), and got as far as the TODO2 below for some as-yet unknown type variable t5.

                         TODO2
------------------------------------------------------------
InR (1, roll (InR (2, roll (InL ())))) :: t5[t := rec t. t5]
------------------------------------------------------------
roll (InR (1, roll (InR (2, roll (InL ()))))) :: rec t. t5
----------------------------------------------------------
unroll (roll (InR (1, roll (InR (2, roll (InL ()))))))
                                     :: t5[t := rec t. t5]

(Note, this validates our intuition that unroll (roll e) should have the same type as e - if it didn't, then the dynamic semantics would not be type safe, via violation of preservation!)

But TODO2 above should just be the partial typing derivation tree we attempted first, unifying t1 + (Int × t4) with t5[t := rec t. t5].

Exercise: Can you complete the typing derivation tree TODO1 and use it to determine what t1, t4, t5 should be, so as to conclude the (common) type of both expressions?

Read on if you want the spoiler straight away:

Answer: Clearly t1 = 1 as we have the unit type for the base (empty list) case.

We can complete TODO1 as follows. To apply the typing rule for roll again, t4 must have the form rec t. t6 for some variable t6, which itself must have the form t7 + t8 to satisfy the typing rule for InR. t8 must then be Int × t9 and t9 must be 1 + t10 to satisfy the typing rules for product and roll respectively.

               () :: 1
           ----------------------------------
           InL () :: 1 + t10[t := rec t. t11]
           ----------------------------------
2 :: Int   roll (InL ()) :: rec t. 1 + t10
------------------------------------------
(2, roll (InL ())) :: Int × (rec t. t9)
------------------------------------------------------
InR (2, roll (InL ())) :: t6[t := rec t. t6] = t7 + t8
--------------------------------------------
roll (InR (2, roll (InL ()))) :: rec t. t6

At this point, we can decide t10 is Int × t to make the required substitution on t10 possible. Resolving the rest of the type variables, and thereby finding t4 has to be rec t. 1 + (Int × t) and t5 has to be 1 + (Int × t), the derivation tree in full looks like:

                                   () :: 1
                               ----------------------------------------
                               InL () :: 1 + Int × (rec t. 1 + Int × t)
                               ----------------------------------------
                  2 :: Int     roll (InL ()) :: rec t. 1 + (Int × t)
                  --------------------------------------------------
                  (2, roll (InL ())) :: Int × (rec t. 1 + (Int × t))
            ------------------------------------------------------------
            InR (2, roll (InL ())) :: 1 + (Int × (rec t. 1 + (Int × t)))
            ------------------------------------------------------------
1 :: Int    roll (InR (2, roll (InL ()))) :: rec t. 1 + (Int × t)
------------------------------------------------------------------
(1, roll (InR (2, roll (InL ())))) :: Int × (rec t. 1 + (Int × t))
---------------------------------------------------------------------
InR (1, roll (InR (2, roll (InL ()))))
                                :: 1 + (Int × (rec t. 1 + (Int × t)))
---------------------------------------------------------------------
roll (InR (1, roll (InR (2, roll (InL ()))))) :: rec t. 1 + (Int × t)
---------------------------------------------------------------------
unroll (roll (InR (1, roll (InR (2, roll (InL ()))))))
                                :: 1 + (Int × (rec t. 1 + (Int × t)))