Notes on introduction to Dependent Types #2

In the last post we reviewed the ideas of dependent types as interpreted from the book "The Little Typer" by Daniel P. Friedman and David Thrane Christiansen, in this post we will continue introducing concepts covered in the book.

Lambda expressions

In the Pie language, functions are created out of lambda expressions, λ is a constructor it takes a list of arguments and a body of the expression:

(λ (a, b)
  (cons a b))

That code constructs a Pair but the type of the whole expression is not yet known because it hasn’t been applied to any arguments, applying a function to arguments is the “eliminator” for functions:

(λ (a, b)
  (cons a b)) 3 5

Now the expression is a (Pair Nat Nat) because it is applied to both 3 and 5 and those are Nats. However it is possible to claim the type of a lambda expression if it’s defined with the define keyword:

(claim maker
  (-> Nat Nat
      (Pair Nat Nat)))
(define maker
  (λ (a, b)
    (cons a b)))

Here, although the lambda expression is not yet applied, we know the type of the expression, is a (-> Nat Nat (Pair Nat Nat)), that is, a lambda expression that takes two Nat to yield a (Pair Nat Nat). Now a little note about sameness; two lambda expressions are said to be the same if their bodies are the same keeping in mind that consistently renaming variables does not change the meaning of the expression.

Neutral expressions

Expressions that contain variables and whose type is not yet known are called neutral expressions and two neutral expressions that are written identically are always the same no matter their type.

Type values

Expressions that have a type constructor at the top are also values, it turns out that Nat, Atom, Pair, -> are all type constructors, some of them take arguments (like Pair and ->) and others don’t, but they all yield Types. In the book we encounter the following definition:

An expression that is described by a type is a value when it has a constructor at its top. Similarly, an expression that is a type is a value when it has a type constructor at its top.

Perhaps my thinking is wrong, but its easier for me to read value constructor when reading just constructor, that helps me to link that there are constructors that take values and yield values (thus a value constructor) and there are constructors that take types and yield types (a type constructor) and in Pie both of these are values, because they have a constructor (either of values or types) at the top.

There we find the following example:

(car
  (cons Atom 'hello))

This is a type, but not a value because it doesn’t have neither a value constructor or a type constructor at its top (car is neither of those, it’s an eliminator). Further more all types are described by U, this is what I believe is a kind but I’m not entirely sure 🤔, let’s read the definition:

Every expression described by U is a Type, but not every Type is described by U.

Yeah, that sounds pretty much like a kind for me. This means that expressions like this:

(cons Atom Nat)

Are not a (Pair Atom Nat) but instead they are a (Pair U U), on the other hand (Pair 'hello 33) is indeed a (Pair Atom Nat) because 'hello and 33 are values, not types.

Types can also be defined, in the book the Pear type is defined like this:

(claim Pear
  U)
(define Pear
  (Pair Nat Nat))

Now wherever a (Pair Nat Nat) is used, a Pear will do just fine, and it means that a (cons 5 10) is a Pear. And this is where we see that definitions are not needed at all, they’re just a convenience that improve our understanding of complex expressions.