More on Existentials

In a previous post I suggested a new (?) interpretation for pattern variables in case branches. This post is my way to understand matters more.

Let's start with the basic example

data Temp :: * where

  Kelvin :: Float -> Temp

Then Kelvin 273.2 is about the temperature at which water freezes (or dually, thaws). Okay, let's demonstrate my point by this code:

diff :: Temp -> Temp -> Bool

diff (Kelvin a) (Kelvin b) = a == b

test t = case t of { Kelvin a -> diff t (Kelvin a) }

What do you expect the function test is? Yes, the const True one! The explanation is simple, as we are in a referentially transparent context, destructuring a value by pattern matching and reconstructing it the same way from its parts creates a value undistinguishable from the original. This of course means that diff will not be able to detect a difference.

Let's switch to a different interpretation. Some oracle invokes the case branch and says: I am not allowed to tell you what it is but here is a Float named a and you can assume that Kelvin a is indistinguishable from t!

Look ma, no 'pattern matching' or 'destructuring' needed!

a may contain 3.14 or 3.15 or 100.1 or ..., ad infinitum, we simply do not know. But we know that it names a Float! It exists as a Float. Mathematically the case branch can be written as

∃a:Float (t ≡ Kelvin a) . diff t (Kelvin a)

which is the english phrase "compute diff t (Kelvin a) under the assumption that there is a Float-valued number that when passed to the function Kelvin becomes undistinguishable from the case scrutinee".

After seeing the same thing in three languages we have to reformulate it one more time. Into logic, that is the language of type theory. Types are propositions and any value one type inhabit proves the corresponding proposition. The existential quantifier (∃) above gets mapped to a dependent sum that is the input to the computation

t : Temp ⊦ 〈a : Float, proof : SomeProp(t, a)〉. diff t (Kelvin a)

I took this formulation (and other wisdom) from Appendix A of Steve Awodey's recent paper. This part unfortunately is not my strongest side. My best guess is that SomeProp(t, a) is a type that encodes the sameness fact, and depends on a. Moreover, proof is an inhabitant of that type. The 〈a : Float, proof : SomeProp(t, a)〉 construct binds two existential variables. The I hope to come up with a nicer formulation sometime. (Please comment if I got something wrong, thanks!)

After understanding this, we can advance to more involved issues, namely one level higher. Take a look at this gorgeous definition:

data Ex :: * where

  Hide :: a -> Ex

This is a pretty useless data type but should be sufficient for my purposes. Then we need a function that pattern matches on it:

f :: Ex -> Bool

f e = case e of { Hide it -> True }

We see that pattern matching unhides the hidden value. It is said that it receives an existential type in the case branch where it is bound. But you will see no type annotation on it, ever.

So, what happens in the case branch this time? While the type of it might have been known at the moment of construction, at this point the type system does not know it. So it is assumed to have some type t. After giving our unknown a name (thus qualifying it existentially) we can ponder about the value of it. This is something we have explored above already, so we can reformulate the case branch mathematically like follows:

∃a:* (true) . ∃it:a (e ≡ Hide it) . True

The first qualifier has just a trivial condition attached to it, I believe I could also have omitted it. I am on pretty thin ice at this point so I'll refrain from giving a type-theoretic transcription, but you can imagine that there will be two dependent sum binders where the first enters in the second in the classifier position.

One more closing thought on the oracles involved. They sound mysterious but they aren't at all. For example in Ωmega the oracle for values it the reduction machinery for runtime values. It is obvious how this machinery is able to look into closures and deconstruct instances of polynomial datatypes. On the type (also kind and up) level, however Ωmega resorts to narrowing, an evaluation mechanism usually employed in logic programming. In the typing rules these mechanisms do not have a place, thus how the variables get bound remains elusive to those.