Dependent type

So in a lot of FP langs you have polymorphic algebraic data types like Maybe:

data Maybe a = Some a | None

It's a type with

• a param,
• two constructors,
  • one of them takes a value of that type param

In a dependent type theory you might see a definition like that, but it’d be syntactic sugar for the more explicit:

Inductive Maybe (a : Type) : Type :=
| Some : a -> Maybe a
| None : Maybe a

Where we instead

• give type signatures for each constructor explicitly,
  • which each need to end in returning the type we’re defining.

Actually in the end the type signatures of the constructors will also include the type parameter:

Some : forall (a : Type), a -> Maybe a

Getting a little trickier, we could also translate a list type:

data List a = nil | cons a (List a)

desugars to

Inductive List (a : Type) : Type :=
| nil : List a
| cons : a -> List a -> List a

Both of these are polymorphic types, or more formally they’re polymorphic type families.

• A group of types related by a common type former and common

polymorphic constructors.

The next step beyond a List type? A length-indexed list type. This I can’t express in ADT notation:

Inductive Vector (a : Type) : nat -> Type :=
| Vnil : Vector a 0
| Vcons : forall (n : nat), a -> Vector a n -> Vector a (1 + n)

Compare this with the definition of List and a few things stand out:

• the signature of the type former has gone from Type to nat -> Type,
• cons has an extra parameter for a length, and
• the constructors no longer have exactly the same return type.

Trying to understand the syntax (this isn't valid, it's just to help me group things logically):

• (Vector int): nat -> Type
• Vector : Type -> nat -> Type

So, the first change: the type former now describes a family not just parameterized by the element type but also by the length.

However, by placing that nat after the :, it’s not scoped over the rest of the constructors as well. (a is)

This is called a type index, and what it means is each of our constructors can now involve multiple members of the type family at once and even determine which one they return.

• Vnil shows that: it specifically returns a value of the 0-length vector types (one for each possible element type).
• Vcons gets even more interesting:
  • like cons it takes a value and a sublist (well, sub-vector).
  • But now it has to be polymorphic in the length of that sub-vector, hence the extra parameter.
  • and it uses an expression to decide its return type:
    • it produces a value of the vector type one longer than its sub-vector.

So,

• Vnil always produces vectors in the 0 length types, and
• Vcons (essentially) increments the type index of its sub-vector at the same time as it collects an additional element.

Those two properties actually enforce the type index being the vector length, in a way that the compiler will keep track of for you.

Skipped a message about the type for a length-preserving map

From these same building blocks we can make things like the family of equality types.

Values of which represent evidence that two expressions will evaluate to the same thing at runtime,

and type families that correspond to inductively defined logical props and relations. I’ll stop here for now tho. 😅

It has a rather nauseating definition at first glance, imo.

Inductive eq (A : Type) (a : A) : A -> Type :=
| eq_refl : eq A a a.

It’s a family of types, where the only inhabited ones correspond to reflexive equalities.

And then there’s usually some notation shenanigans so we can use = instead 😅

Reserved Notation "_ = _" (at level 70, no associativity).
Inductive eq {A : Type} (a : A) : A -> Type :=
| eq_refl : a = a
where "a = b" := eq a b.

The {} mean that parameter should be inferred automatically, because it’s constrained/redundant by the types of the later parameters. You only ever use eq with values, so A can always be inferred as the type of those values.

So, you can only construct things like eq_refl 5 : 5 = 5. Where that gets useful is the really funky way that type indexes interact with pattern matching- this is “dependent pattern matching”.

If you have some H : a = b (constructed… somehow, I can get to that 😅) and pattern match on it the only possible branch will be eq_refl a. Except, the type of eq_refl a is a = a. What that means is, on that branch you “learn” (in a way the type checker can understand) that actually b must have been a all along. A similar thing happens if you pattern match on a vector of some generic length- on the Vnil branch you “learn” that that length was actually 0 all along, and on the Vcons branch you learn that the length is actually 1 + some smaller length. That substitution impacts the types of other values you have, refining your understanding of them. For example, say if you have two vectors that share the same length and pattern match on one of them. V1 V2 : Vector A n and you pattern match on V1. Well, on the Vnil branch you learn that n is 0. That also means that on this branch V2’s type is really Vector A 0. Similarly, on the Vcons branch you learn that n is really 1 + m (for some m that you got from the pattern matching). Well, now V2’s type can be refined to Vector A (1 + m) too.

Returning to eq, if you have a V : Vector A n and an H : 5 = n you can actually pattern match on H. There will be exactly one branch, but on that branch you’ll learn that n must really have been 5 all along! And so, you get to refine the type of V to Vector A 5. This all comes down to how the individual constructors get to specify the values of the type indexes they return: when you pattern match and end up on the branch corresponding to that constructor you also learn that actually whatever you had for that index must be interchangeable with whatever that constructor puts there. Otherwise you wouldn’t have made it to that branch, that constructor would not have been usable to construct that value. You can’t construct a Vnil whose length is non-0, and you can’t construct a Vcons whose length is 0. And you can’t construct an eq_refl where a and b are different.

When you pattern match on a value of an indexed type you get to do substitutions on the expression for the index in the types of other stuff.

In V1 V2 : Vector A n, n is an index. So, if you pattern match on V1 you get to substitute n with other stuff in any other types where it appears (like the type of V2)

The thing you get to substitute it with? Well, on each branch the constructor will give an expression of its own for the index. You get to substitute n with that. With eq, the LHS is a parameter and the RHS is an index.

So when you have H : 5 = n, 5 is the param and n is the index.

When you pattern match on it you’ll have exactly one branch where you reveal it must have been constructed by eq_refl and where the index is given as whatever the parameter was.

So you get to substitute n with 5 in any other types.

That’s why, btw, I specifically wrote it 5 = n instead of the other way around. You can write a symmetry helper, but I didn’t want to introduce that yet lol The “primitive” operation is specifically replacing whatever’s on the right side with whatever’s on the left side.

I also did a similar bit of slight of hand using 1 + n in the definition of Vector, for technical reasons that will probably make your eyes glaze over at this stage 😅