A Taxonomy of Self-Types

Part I: Introduction to Self-Types

Datatypes in the Formality programming language are built out of an unusual structure: the self-type. Roughly speaking, a self-type is a type that can depend or be a proposition on it's own value. For instance, the consider the 2 constructor datatype Bool:

T Bool
| true
| false

This corresponds to the Haskell datatype

data Bool = True | False

However, in Formality, the above T datatype syntax is not primitive, but is desugared to the following Formality-Core expressions:

Bool: Type
  bool(P: Bool -> Type) ->
  (true  : P(Bool.true)) ->
  (false : P(Bool.false)) ->
  P(bool)

Bool.true: Bool
  (P) (t) (f) t

Bool.false: Bool
  (P) (t) (f) f

Actually the real Formality-Core differs very slightly from this due to runtime erasure, but for the purposes of this explantion that can be ignored.

Formality-Core is a very simple, but surprisingly expressive language. In the above definition of Bool, the following constructors are used

Dependent function type: (x: A) -> B(a)
Lambda: (x) b
Application f(x)
Reference: any name, such as Bool.true, that is not bound by a dependent function or a lambda refers to a top-level exprssion.

The difference between an ordinary function type and a dependent function type is that the former must always return the same type, whereas the latter can return values of different types depending on the input value.

For example:

elim_bool.type: Bool -> Type
  (bool) bool(() Type)(Unit)(String)

elim_bool: (bool: Bool) -> elim_bool.type(bool)
  (bool) bool((b) elim_bool.type(b))(Unit.new)("a string")

In the above elim_bool(Bool.true) would return Unit.new :: Unit, whereas elim_bool(Bool.false) would return "a string" :: String (: and :: are both type annotations).

To understand the definition of Bool in Formality-Core, we first have to understand the notion of dependent elimination. In Haskell, ordinary non-dependent elimination is a case expression:

caseBool :: Bool -> String
caseBool bool = case bool of
  True  -> "The True case"
  False -> "The False case"

"Elimination" here means that we eliminated the input type by transforming it into some other type. The elim_bool Formality-Core function is an example of dependent elimination because the we transformed the Bool into different types Unit and String for different cases.

caseBool :: Bool -> String
caseBool bool = case bool of
  True  -> "The True case"
  False -> "The False case"

In the Idris programming language, which is similar to Haskell but has dependent types, we could write

data Bool = True | False

elimBool : (b : Bool) -> (elimBoolType b)
elimbool bool = case bool of
  True  => ()
  False => "a string"

elimBoolType : Bool -> Type
elimBoolType bool = case bool of
  True  => ()
  False => String

Notice how we have to have three separate definitions for the datatype, the dependent eliminator, and the type of the eliminator.

There's a redundancy here if you consider that in the pure untyped lambda calculus, you can encode the values of Bool as their own eliminators using the Church encoding

true  = λx λy. x
false = λx λy. y

elimBool b = (b () "a string")

Here if you apply elimBool to true, you'll get the unit value, and if you apply it to false you'll get the string value. This can be convenient in an untyped language, but it's a little unclear to see how we could assign types to these expressions, if we wanted Church encodings without giving up static types:

true : a -> b -> a
true  = λx λy. x

false : a -> b -> b
false = λx λy. y

elimBool : ?
elimBool b = (b () "a string")

Since elimBool has to describe the type of its input b, we would have to have a way to make a type that contains both a -> b -> a and a -> b -> b. (In Haskell or Idris you could use an Either type to due this, but then elimBool would have to case match on Either. We're trying to encode datatypes as eliminators so we don't need primitive case expressions.)

That's exactly what self-types do. They allow you to build a type that can be a -> b -> a if you're trying to type true = λx λy. x and a -> b -> b if you're trying to type false = λx λy. y.

Let's look at the definition of Bool in Formality-Core again:

Bool: Type
  bool(P: Bool -> Type) ->
  (true  : P(Bool.true)) ->
  (false : P(Bool.false)) ->
  P(bool)

Bool.true: Bool
  (P) (t) (f) t

Bool.false: Bool
  (P) (t) (f) f

The bool name is the self-type, which can be thought of as an extension of a dependent function to allow the output of the function to depend not only on the input values, but also on the value of the term being typed.

Bool is a dependent function with three inputs:

Another function P that takes a Bool value and returns a Type (like Foo.type). Functions that take values of a type and return Type are also called "propositions" (hence the name P) over that type.
A value that is the type of proposition P over Bool.true
A value that is the type of proposition P over Bool.false

The value returned by Bool is proposition P over whatever the value of the bool :: Bool is.

Bool.true and Bool.false are almost exactly the standard Church encodings described above, but there's an additional argument P (which actually gets erased at runtime).

We can even just substitute the references directly inline in the type:

Bool: Type
  bool(P: Bool -> Type) ->
  (true  : P((P) (t) (f) t) ->
  (false : P((P) (t) (f) f) ->
  P(bool)

Or we can substitute the type into the term level constructors:

true: bool(P: Bool -> Type) -> P((P) (t) (f) t) -> P((P) (t) (f) f) -> P(bool)
  (P) (t) (f) t

false: bool(P: Bool -> Type) -> P((P) (t) (f) t) -> P((P) (t) (f) f) -> P(bool)
  (P) (t) (f) f

This should help explain how the elim_bool function we described above works:

elim_bool.type: Bool -> Type
  (bool) bool(() Type)(Unit)(String)

elim_bool: (bool: Bool) -> elim_bool.type(bool)
  bool((b) elim_bool.type(b))(Unit.new)("a string")

In elim_bool.type, P is () Type i.e. the constant function that throws away its input and returns Type :: Type. Then Unit :: Type, so Unit :: P(Bool.false) and String :: Type so String :: P(Bool.true).

In elim_bool, we depend on the the value of the bool, so our propositon P is (b) elim_bool.type(b)

And that's how self-types work in Formality. They allow us to create a type for all the dependent eliminators of a datatype, which then means we can encode the datatype itself as the type of its eliminators.

Part II: A taxonomy of self-type encodings

The self-type encodings described in the previous section are expressive, in many ways more expressive than the datatype primitives of other languages.

The family of Variant encodings

For example, the Bool (here with erasure of arguments that do not appear at runtime using the <> syntax) type described in the previous section can be extended into a family of encodings of simple sum or variant types:

-- simple variant type #0
-- T Empty
Empty: Type
  empty<P: Empty -> Type> ->
  P(empty)

-- simple variant type #1
-- T Unit
-- | unit
Unit : Type //prim//
  unit<P: Unit -> Type> ->
  (new: P(Unit.new)) ->
  P(unit)

Unit.new : Unit
  <P> (unit) unit

-- simple variant type #2
-- T Bool
-- | true
-- | false

Bool: Type
  bool<P: Bool -> Type> ->
  (true  : P(Bool.true)) ->
  (false : P(Bool.false)) ->
  P(bool)

Bool.true: Bool
  <P> (t) (f) t

Bool.false: Bool
  <P> (t) (f) f

-- simple variant type #3
-- T Trit
-- | yes
-- | unknown
-- | no

Trit: Type
  trit<P: Trit -> Type> ->
  (yes     : P(Trit.yes)) ->
  (unknown : P(Trit.unknown)) ->
  (no      : P(Trit.no)) ->
  P(trit)

Trit.yes: Trit
  <P> (y) (u) (n) y

Trit.unknown: Trit
  <P> (y) (u) (n) u

Trit.no: Trit
  <P> (y) (u) (n) n

We can start to see how we could make the 4th, 5th or nth simple variant type.

VariantN : Type
  variantN<P: Variant_N -> Type> ->
  (n_1 : P(VariantN.1)) ->
  ...
  (n_n : P(VariantN.n)) ->
  P(variantN)

VariantN.1 : VariantN
  <P> (x1) ... (xN) x1
...
VariantN.n : VariantN
  <P> (x1) ... (xN) xN

Let's call this the Variant family of self-type encodings.

The Abstract family of Self-Type encodings

We can not only encode simple variants, but also abstract datatypes with product types (including recursively defined types):

-- Church encoded natural numbers
Nat: Type
  nat<P: Nat -> Type> ->
  (zero: P(Nat.zero)) ->
  (succ: (pred: Nat) -> P(Nat.succ(pred))) ->
  P(nat)

Nat.zero: Nat
  <P> (z) (s) z

Nat.succ: Nat -> Nat
  (n)
  <P> (z) (s) s(n)

-- Church encoded lists
List: (A: Type) -> Type
  (A)
  list<P: (x: List(A)) -> Type> ->
  (nil: P(List.nil<A>)) ->
  (cons: (head: A) -> (tail: List(A)) -> P(List.cons<A>(head)(tail))) ->
  P(list)

List.cons: <A: Type> -> (head: A) -> (tail: List(A)) -> List(A)
  <A> (head) (tail)
  <P> (nil) (cons) cons(head)(tail)

List.nil: <A: Type> -> List(A)
  <A>
  <P> (nil) (cons) nil

Constructing a member of the Abstract family can be done by beginning with the nth member of the Variant family and adding:

t type parameters
arguments to each constructor, where the ith constructor receives ki arguments with type Ai.ki

AbstractN : <T1 : Type> -> ... -> <Tt : Type> -> Type
  abstractN<P: Abstract_N -> Type> ->
  (absN.1 : (a1.1 : A1.1) -> ... -> (a1.k1: A1.kn) ->
            P(AbstractN.1<T1>...<Tt>(a1.1)...(a1.k1))
  )->
  ...
  (absN.n : (an.1 : An.1) -> ... -> (an.kn: An.kn) ->
            P(AbstractN.N<T1>...<Tt>(an.1)...(an.k1))
  )->
  ...
  P(abstractN)

AbstractN.1 : <T1: Type> -> ... -> <Tt : Type> ->
              (a1.1: A1.1)  -> ... -> (a1.k1: A1.k1) ->
              AbstractN.1<T1>...<Tt>(a1.1)...(a1.k1))
  <T1> ... <Tt>
  (a1.1) ... (a1.a1)
  <P> (x1) ... (xN) x1(a1.1)...(1.a1)
...
AbstractN.n : <T1: Type> -> ... -> <Tt : Type> ->
              (an.1: An.1)  -> ... -> (an.kn: An.kn) ->
              AbstractN.1<T1>...<Tt>(an.1)...(an.kn))
  <T1> ... <Tt>
  (an.1) ... (an.kn)
  <P> (x1) ... (xN) x1(a1.1)...(an.kn)

This starts to get very complicated, since within this family structure are all abstract datatypes that can be formed using sum types (which correspond to constructor variants) and product types (which correspond to constructor arguments).

The Algebraic family of encodings

However we can go further. The types of the constructors arguments in the Abstract family need not be constants, they can themselves depend on the constructor arguments and type parameters. This family corresponds to generalized algebraic datatypes (GADTs):

Subset: (A: Type) -> (B: A -> Type) -> Type
  (A) (B)
  subset<P: Subset(A)(B) -> Type> ->
  (make: (a: A) -> <b: B(a)> -> P(Subset.make<A><B>(a)<b>)) ->
  P(subset)

Subset.make: <A: Type> -> <B: A -> Type> -> (a: A) -> <b: B(a)> -> Subset(A)(B)
  <A> <B> (a) <b>
  <P> (subset)

For brevity, we will avoid writing out the ... skeleton as before (since it gets quite illegible), but to construct this family, begin with a member of the Abstract famliy and add arguments to any of the Ai.ki constructor argument types.

The Indexed family of encodings

Self-type encodings can depend on the values of other self-types, in a process called type-indexing. For example, this Word type contains a type-level Nat natural number describing how many bits the Word contains. A Word(Nat.32) for example contains exactly 32 bits (anything else being a type-error).

Word: Nat -> Type
  (size)
  word<P: (size: Nat) -> Word(size) -> Type> ->
  (we: P(Nat.zero)(Word.nil)) ->
  (w0: <size: Nat> ->
       (pred: Word(size)) ->
       P(Nat.succ(size))(Word.0<size>(pred))
  ) ->
  (w1: <size: Nat> ->
       (pred: Word(size)) ->
       P(Nat.succ(size))(Word.1<size>(pred))
  ) ->
  P(size)(word)

Word.0: <size: Nat> -> Word(size) -> Word(Nat.succ(size))
  <size> (wo) <P> (we) (w0) (w1)
  w0<size>(wo)

Word.1: <size: Nat> -> Word(size) -> Word(Nat.succ(size))
  <size> (wo) <P> (we) (w0) (w1)
  w1<size>(wo)

Word.nil: Word(Nat.zero)
  <P> (we) (w0) (w1)
  we

Part III: Mutant encodings

You might think at this point that we're done. Not even close. The families of datatype encodings described above form a super-family of "Standard" self-types, but these are the vast minority of all the possible valid encodings that can be generated.

For instance, consider the Bool type again:

Bool: Type
  bool(P: Bool -> Type) ->
  (true  : P(Bool.true)) ->
  (false : P(Bool.false)) ->
  P(bool)

Bool.true: Bool
  (P) (t) (f) t

Bool.false: Bool
  (P) (t) (f) f

What happens if when we're typing this in we accidently type t instead of an f in the body of Bool.false

MutantBool: Type
  mutantBool(P: MutantBool -> Type) ->
  (true  : P(MutantBool.true)) ->
  (false : P(MutantBool.false)) ->
  P(mutantBool)

MutantBool.true: MutantBool
  (P) (t) (f) t

MutantBool.false: MutantBool
  (P) (t) (f) t

Amazingly, this typechecks, and corresponds to an eliminator with irrelevant arguments:

elim_mutant_bool.type: MutantBool -> Type
  (bool) bool(() Type)(String)(String)

elim_mutant_bool: (bool: MutantBool) -> elim_mutant_bool.type(bool)
  (bool) bool((b) elim_mutant_bool.type(b))("true")("false")

If you try the following, you will see that regardless of the input, the elimination returns a constant "true"

elim_mutant_bool.test : String
  elim_bool(MutantBool.false)

Even more excitingly, elim_mutant_bool.type will now type error if you try to construct a dependent function with:

elim_mutant_bool2.type: MutantBool -> Type
  (bool) bool(() Type)(String)(Unit)

elim_mutant_bool2: (bool: MutantBool) -> elim_mutant_bool2.type(bool)
  (bool) bool((b) elim_mutant_bool2.type(b))("true")(Unit.new)

Because of course elim_mutant_bool2 returns constant String, since it throws away the second argument regardless of input.

Had we defined Mutant bool with f in both constructors, we could have constructed the constant "discard first argument" eliminator

Illegal mutants

The fact we can construct "discard first", "discard second" mutant eliminators as well as the regular Bool raises the question of whether we can construct the eliminator that chooses the case from its opposite branch. This turns out to be impossible:

Illegal: Type
  ill(P: Illegal -> Type) ->
  (true  : P(Illegal.true)) ->
  (false : P(Illegal.false)) ->
  P(ill)

Illegal.true: Illegal
  (P) (t) (f) f

Illegal.false: Illegal
  (P) (t) (f) t

The type contains a contradiction, which becomes apparent if we inline the type:

true: ill(P: Bool -> Type) -> P((P) (t) (f) f) -> P((P) (t) (f) t) -> P(ill)
  (P) (t) (f) f

The self type ill here refers to the term (P) (t) (f) f, but the body f has type P((P) (t) (f) t), which not an equal term.

This result is extensible to any Variant family encoding (and maybe beyond):

For every constructor the return value must correspond to
- itself, when constructor i returns argument i
- a term equal to itself, when constructor i returns argument j, with MutantN.i == MutantN.j

For example, for Variant3:

TritM: Type
  trit<P: TritM -> Type> ->
  (yes     : P(TritM.yes)) ->
  (unknown : P(TritM.unknown)) ->
  (no      : P(TritM.no)) ->
  P(trit)

TritM.yes: TritM
  <P> (y) (u) (n) y

TritM.unknown: TritM
  <P> (y) (u) (n) y

TritM.no: TritM
  <P> (y) (u) (n) n

is permitted, but y,n,y or n,y,u etc. creates a contradiction.

The number of legal Variant self-type encodings for every n corresponds to the number of pointed set partitions of cardinality n, which is OEIS sequence A000248.

A Haskell generator for all the candidate Variant self-type encodings of cardinality n can be found here: https://gist.github.com/johnchandlerburnham/fe53c5702bca6f0925f344905e82c0b0

Future exploration

The Mutant family of self-types is of particular interest given the relationship between set partitions, equivalence relations, and Higher-Inductive-Types. In fact, the OEIS sequence linked above is described as:

Let set B have cardinality n. Then a(n) is the number of functions f:D->C over
all partitions {D,C} of B.

a(3)=10 since, for B={1,2,3}, we have 10 functions: 1 function of the type
f:empty set->B; 6 functions of the type f:{x}->B\{x}; and 3 functions of the
type f:{x,y}->B\{x,y}.

Since any partition of a set forms an equivalence relation, if self-types somehow encode equivalence relations, then perhaps there is some undiscovered construction which will enable structures like the higher inductive Interval type:

Inductive interval : Type :=
| zero : interval
| one : interval
| segment : zero == one.

from Homotopy Type Theory, which is essentially a 2-set with a custom equivalence relation.

However, preliminary work indicates that MutantBool itself is likely not a valid Interval type, since the attempting to derive extensional equality from it via (Jason Gross' technique)[https://people.csail.mit.edu/jgross/CSW/csw_paper_template/paper.pdf] fails. The issue is that because we define self-types as in Formality through a term's "action as an eliminator", our self-type encoded Equal type requires that the equal terms inside it have the same eliminator action.

// The Equal datatype.
// T Equal<A, x: A>(b: A)
// | Equal.to : Equal(A, a, a)
Equal: (A: Type) -> A -> A -> Type
  (A) (a) (b)
  equal<P: (b: A) -> Equal(A)(a)(b) -> Type> ->
  (to: P(a)(Equal.to<A><a>)) ->
  P(b)(equal)

Gross' proof requires that the zero : Interval and one : Interval be somehow equal, but have different eliminator action. My attempted port of Gross' proof is (here)[https://gist.github.com/johnchandlerburnham/0e37c0cb265aa67355892e32cb9579f8]

The open question then is whether there exists a way to encode equality in Formality-Core that does not impose equality of eliminator action (perhaps not even using self-types). If so, and if we can further show that such an alternate equivalence is itself equivalent (but not equal) to Equal, then perhaps the axiom of univalence can be constructed in Formality. That would be extremely exciting.

johnchandlerburnham/ATaxonomyOfSelfTypes.md