Under false pretenses

[empty-types] [equality]

The empty type 00 has no values, so a variable x:0x : 0 can never be supplied. So, any code within the scope of such a variable can never be executed. (For a lazy language like Haskell, read "underneath a case split on" instead of "within the scope of").

In such unreachable scopes, many type systems become a little strange. This strangeness is not by itself a problem, as it can only arise in unreachable code, but care must be taken to keep it contained.

For example, it is possible in such a scope to construct an expression of a equality type, "proving" that Int\n{Int} and String\n{String} are equal:

type empty = |
type (_,_) eq =
  Refl : ('a, 'a) eq
let f (x : empty) =
  let eq : (int, string) eq = match x with _ -> . in
{-# LANGUAGE EmptyCase #-}
data Empty
data Eq a b where
  Refl :: Eq a a

f :: Empty -> ...
f x = ...
    eq : Eq Int String
    eq = case x of {}

If use of eq introduces the equation Int=String\n{Int} = \n{String}, then you may end up with nonsensical expressions such as 20 - "hello" becoming well-typed. This can interfere with compiler optimisations: the constant folding optimisation eagerly computes arithmetic operations whose arguments are constant, and may not be able to handle, say, subtraction of a string from an integer, even in dead code. Generally, hoisting optimisations (those which move an expression to an earlier position) must be treated carefully, as they risk moving a nonsensical computation from dead code to code that actually runs.

In type systems based on Martin-Löf's Intensional Type Theory, a more subtle issue can arise. ITT-based systems have a relation ABA ≡ B called definitional equality (or judgemental equality). Definitional equality determines which expressions are considered "obviously equal" (that is, can be substituted for each other in any context with no explicit coercion required), and part of the design of an ITT-based type system is to decide which rules can be included in while keeping the relation decidable.

In the presence of an empty type 00, it is tempting to make any two functions f,g:0Af, g : 0 → A definitionally equal, as there is only one possible function from 00 to any type. However, as noted by McBride1, this choice breaks decidability of , because under the scope of a variable x:0x : 0, we have: true(λ(y:0).true)x(λ(y:0).false)xfalse \n{true} ≡ (λ (y : 0). \n{true}) x ≡ (λ (y : 0). \n{false}) x ≡ \n{false}

So, in order to decide whether truefalse\n{true} ≡ \n{false}, we would first need to decide whether the type of any variable in scope is or can be converted to 00, which is not in general decidable.


Grins from my Ripley Cupboard, Conor McBride, 2009.