Within dependently typed languages such as Idris types:

- are
*first-class* - can
*depend on values*; and - can be computed.

With this last point we see that the Idris language doesn’t have special constructs to specify type synonyms: We write functions to compute the type.
Similarly, we can compute type signatures from programs.
A common example seen is the type-safe `printf`

function in which an EDSL describes the format string and is then computed to construct a type signature.

In this post I want to show how we can use dependent types to compute simple type signatures.

## A Data Type for Type Signatures

First we define `Typer`

a simple indexed algebraic data type to represent a type signature.

We use `Let`

to represent sequencing of expressions.
`Return`

indicates the function’s return type, and `Param`

represents a function parameter that *might* have documentation.
`SemiColon`

signifies the end of the signature.

Now this is not the best representation for this data type!
We can present multiple returns declarations, and said declarations can be interleaved between parameters.
We can revisit the type of `Typer`

to introduce more machinery to reason about the substructural properties of `Typer`

, but I leave that as an exercise for the reader.

To get Idris’ Do-notation we use `Let`

as an implementation for `(>>=)`

.

With `Typer`

we can specify simple functions that compute concrete type signatures.
I haven’t looked at how we can construct polymorphic type signatures.

### Examples

We can use `Typer`

to write type signatures.

#### Append

#### Concat

In this next example we present the definition of a function to concatenate two lists with length.

#### Minnie

In our last example we present the signature for a function that returns a dependent pair such that the value returned is the minimum value of the two presented arguments.

## Compiling Typer

We can use `Typer`

to compute a continuation based data structure (`AType`

) to describe our type signature.
We can then use `AType`

instances to build type signatures.
We define `AType`

as follows:

`AType`

represents a continuation that sequences a series of parameters (`P`

) and ends with a return type `R`

.
We need `Stop`

here for totality reasons even though the continuation ends with `R`

.
We can build `AType`

instances using `Typer`

using the following function:

As types are first class We can execute (*run*) `AType`

instances to compute real type signatures.

Notice how we bind the name of a parameter to a value and pass it on to help compute the next argument or return type.
We can combine `build`

and `run`

into `type`

to make lives easier.

We need `Stop`

here to provide a termination point to the signature, as we don’t know what the final return type will be.
This mirrors the role of `SemiColon`

.

Using `type`

we can compute the concrete type signatures for our previous examples.

## Now for something completely different

Rather than compute concrete type signatures we can define a secondary Resource Dependent EDSL to use `AType`

instances as a contract to help ensure that a program’s arguments and return type match the specification.
In a way this is type-checking a program by construction^{1}.

We define `Prog`

our EDSL within a `namespace`

to allow constructor name reuse^{2}.

`Prog`

is a resource dependent EDSL that computes `AType`

instances within its type.
This ensures that the sequencing of data constructors **must** match the ordering as presented by an `AType`

continuation.

`Let`

allows us to sequence expressions and ensures that the continuation embedded within `AType`

is correctly executed.
`Pure`

is the return value and it’s value **must** have the same type as presented by the `R`

constructor of `AType`

.
It’s next state is `Stop`

.
`Arg`

represents a parameter and as with `Pure`

it’s value **must** have the same type as specified by the `P`

constructor of `AType`

.
Further, the type of `Prog`

and the continuation embedded within the constructor `P`

represents the next value in the sequence.
`SemiColon`

is required to provide a termination point to the function body.

Notice that `SemiColon`

has to be provided after a `Pure`

constructor, and that we can only get to a `Pure`

constructor by stepping through the continuation embedded within `AType`

.
This is how the ordering (sequenced using `Let`

) in `Prog`

is dictated by `AType`

.

We provide implementations, as required, to `(>>=)`

and `pure`

for Do-notation.

We can now construct a function `typeDef`

to dictate the initial and final states of a `program`

.

`typeDef`

uses the provided specification to `build`

an `AType`

instance that represents the initial state with final value of `Stop`

, and we ask that our final state is `Stop`

.

### An Example

We finish with an example that uses `Append 4 3 Nat`

as a specification to type check against.

## Coda

This was a simple example on how to use dependent types to do some interesting computations relating to constructing program specifications, and subsequently verification an implementation against a specification.
We can extend the example in many ways to tighten the specification correctness but also enhance the expressiveness of our programs.
I reckon we could do something interesting with this construction, as to how interesting for publication I am not sure.
Sometimes, it is hard for me to tell if what I do is truely novel, or for another Dependently Typed Programmer to go: *this is just x*.

Regardless, the example construction here is a popular design pattern within my Idris programs to provide an intrinsic link between a specification and an implementation. I learned the pattern from a dependent typer I met in a bar, and rather truthfully I am not sure how interesting it would be to write this up with them.