Extremal types in Unison

unison_type_hierarchy_notes.md

The type system of Unison is a form of predicative system F, but the intent of this article is not to discuss the type system formally, but to give some understanding for how "extremal types" function within the type system. Extremal types in this sense are types at the bottom or top of some hierarchy, and it should be noted that extremal is not a word used elsewhere in this exact sense, to our knowledge.

Unison Type Hierarchy (lattice of types)

The lattice of types in Unison has top and bottom types:

⊤ = ∃e.e -- Called Any
⊥ = ∀a.a -- Called Void

The meaning and use of these types will be described in more detail below, but for those familiar with object-oriented programming, ⊤ is essentially the supertype of all types, whereas ⊥ is the subtype of all types.

The type system of Unison is a form of predicative system F, see elsewhere for more authoritative sources.

In the Category of types, Void is instead at the top (the initial object), and the Unit type, which is simply the type that has a single occupant (called unit), is at the bottom (called the terminal object).

Let's attempt to show that the following type is equivalent to Any:

∀r∀a(a -> r) -> r

Let r = Void, where ¬ x ≅ x -> Void ≅ x => Void. Then ∀a(a -> Void) -> Void = ¬(∀a(¬a)), that is, it is not true that for all a, not a is true (where not a means a is uninhabited). So then there ∃e(e).

More generally, this typechecks in Unison, showing you can encode existentials with universals:

type Any = Any (forall r . (forall a . a -> r) -> r)

use Any Any

any : a -> Any
any a = Any (k -> k a)

consume : (∀ a . a -> r) -> Any -> r
consume f a = case a of Any e -> e f

Here, Any wraps a type that is equivalent to ∃e(e), since, as the any function shows, any type can be passed in to yield a value of type Any:

any5 : Any
any5 = any 5

  
    75 | > any5
           ⧩
           Any.Any (k -> k 5)

consume demonstrates the extent to which we can use a value of type Any, which is to say, not very much:

> any5

c1 = consume (x -> "foo") any5

> c1

Yields

    79 | > c1
           ⧩
           "foo"

We can walk through the logic by substitution, where we see that consume amounts to applying a constant function on the value wrapped in Any:

e f
(k -> k 5) f
(k -> k 5) f
(k -> k 5) (x -> "foo")
-- evaluating:
(x -> "foo") 5 == "foo"

You should always be able to recover a super-type from a subtype, and any, shows that we can always get Any (≅ ∃e(e)) back from any type.

Interestingly, the above encoding didn't need to make use of Void directly. Here's a very informal way of showing that the universally quantified type wrapped in Any above implies existentials, using first-order logic and some handy-wavy application of the Curry-Howard isomorphism (specifically, again ¬x ≅ x → Void ≅ x ⇒ Void). Abuse of notation is also used: ∃e(e) means ∃e(P(e)) where P(e) is the predicate meaning there exists a value of type e.

∀r[∀a(a ⇒ r) ⇒ r]
∀r∀a(a ⇒ r) ⇒ ∀r(r)
∀r∀a(a ⇒ r) ⇒ Void
¬∀r∀a(a ⇒ r)
∃r[¬∀a(a ⇒ r)]
∃r[∃a(¬(a ⇒ r))]
∃r[∃a(¬(¬a∨r))]
∃r[∃a(a∧¬r)]
∃r[∃a(a)∧¬r]     (provable identities)  
∃r[∃a(a)]        (eliminate conjunction) 
∃a(a)            (eliminate redundant quantifier) 

Examples

Relationship to delayed computations

In the language reference, it is stated that

An expression can appear delayed as 'e, which is the same as _ -> e. If e has type T, then 'e has type forall a. a -> T. If c is a delayed computation, it can be forced with !c, which is the same as c (). The expression c must conform to a type () -> t for some type t, in which case !c has type t.

Here, we see that thought the delayed comutation has type forall a. a -> T, it is required to conform to type () -> T. But forall a. a can conform to any type, so this is not an issue.

A note on the Void type

We can construct a wrapper for Void in Unison to more easily refer to it in certain contexts. As shown below, it is not easily possible to construct a Void value. Indeed, it should be impossible to supply a value that is a member of every type:

  The 1st argument to the function Void.Void is Nat, but I was expecting a:
  
     43 | type Void = Void (forall a. a)
     44 | 
     45 | use Void Void
     46 | 
     47 | x: Void
     48 | x = Void 5
  

While we can't use the Void type directly, it can be used in the signature of functions. If Void occurs in argument position, then the function can't be called:

absurd : forall a. Void -> a
absurd _ =
   never _ = !never
   !never

We use the non-terminating function never as the implementation, since there is currently no undefined in Unison (but there likely will be similar builtins in the future, currently named todo and crash). Note that never has signature never: forall a. () -> a, but it wasn't necessary here. We want local scope for never, since it isn't a very good function to call in practice, unless you want a quick and easy way to heat up your CPU!

absurd is one side of the isomorphism between Void and forall a. a. The other side would be any function returning Void (which is impossible), such as a non-terminating function (e.g. never). This should be particularly apparent since absurd and never even have identical implementations!

Similar concepts exist in Haskell and Scala, for instance.

Relationship between Any and Unit

In a sense, values of type Any and unit (the only value of type Unit) intuitively seem to have some similarities. You can't extract any information from either type, and you can easily create inverse functions between the two types:

f: Any -> Unit
f a = unit

g: Unit -> Any
g u = any u

Any place you could use an Any, you could really also use a Unit, or vice versa, by calling one of the above functions. However, the two types are not isomorphic, since |Any| is obviously much larger than |Unit| (if we can even discuss the cardinality of Any, we can say it is at least infinite).

This is interesting since Any is at the at the top of the lattice of types, and Unit is at the bottom (the terminal object) of the Category of Unison types. Void, on the other hand, occupies opposite places in these structures.

Another way to think about this, take Any (exists e . e): "I have a value of some type, but I won't tell you what type it is". Well, if you haven't told me the type, I can't do anything with such a value, unless I have a function which works for all types, that is, is forall e . e -> something. But by nature, such a function can do very little indeed.