# 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 `Nat`

s. 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

is a Type, but not every Type is described byU.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.