Various Notes

• Rob S will take over lecturing in coming lectures. Please make Rob welcome.
• Marking of A0 is taking longer than we hoped, obviously.
  • The lecturers and tutors are hard at work on this.
• About Hindsight:
  • Hindsight is really not a good language to write by hand. The expectation is that control operations like thunk/force/reduce/produce are inserted automatically.
• Testing a1 at CSE:
  • There is now a test script: "3161 test a1_25T3 <files.hs>"
  • The test script just runs the tests you have in the CSE environment.
  • The process uses a local download cache and a temporary location that doesn't use disk quota, but otherwise builds a Cabal setup from scratch. We were hoping to cache more but that wasn't possible.
  • This is too inefficient for normal work.
  • Feel free to test the test script, or inspect how the tests in /home/cs3161/public_tests work.

Here is some ugly MinHS syntax that tries to evaluate (1 + 2) + 3 lazily:

main :: F Int
  = let
    x :: U (F Int) = thunk (1 + 2);
    y :: U (F Int) = thunk (reduce force x to x2 in x2 + 3);
  in produce 5

We have seen a type called () in Haskell. This is sometimes called "unit" or "1" in related languages. It has exactly one element, which in Haskell is also written ().

We will see in the next lecture that "a + unit" (written "Either a ()" in Haskell) has one more element that type "a", and that "a x unit" (written "(a, ())" in Haskell) has the same number of elements as "a".

A related idea is a type "0" which has 0 elements, such that "a + 0" has as many elements as "a", and "(a, 0)" also has 0 elements. This type is sometimes also written "False". It should have no elements, so getting a value of that type indicates that something has gone wrong, or that we are already in an impossible case. A function that takes a value in "False" is a bit like a proof that assumes "False": not very useful.

Partial functions like "head" in Haskell are incompatible with this type.

-- This is perfectly OK.
impossible :: 0 -> a

-- What elements are in [0]?
f :: [0] -> Int
f xs = case xs of
  [] -> 12    -- This does exist
  (y : ys) -> impossible y     -- This case is impossible

-- Note the contradiction with Haskell
-- In Haskell, head :: [a] -> a

-- This is fine.
xs :: [0]
xs = []

-- This produces a contradiction.
x :: 0
x = head xs

These partial functions mean that nothing can really be impossible in the type system, which is perhaps not we want, so they should be used carefully.

Progress and preservation are a canonical way of showing that a type system works for some language. However, some modern authors don't like the approach.

A type system is just a logic for proving something about a program, typically a fast but weak logic, which makes decisions quickly but has to be over-conservative in many cases because of its imprecision. From this perspective, type safety is just "soundness" of the logic, the argument that its claims are true in the semantics. The logic is nearly always "incomplete".

The usual approach to preservation and progress defines the type system on the syntax. The syntax is then interpreted untyped in the semantics. Some modern authors prefer to keep the types in every implementation and semantics. This leads to a formulation similar to "syntactic type-correctness implies semantic type-correctness".