Computing Types with Idris & Linking Specifications with Implementations.

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

We define Prog our EDSL within a namespace to allow constructor name reuse².

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.