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.
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
Typer we can specify simple functions that compute concrete type signatures.
I haven’t looked at how we can construct polymorphic type signatures.
We can use
Typer to write type signatures.
In this next example we present the definition of a function to concatenate two lists with length.
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.
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.
AType as follows:
AType represents a continuation that sequences a series of parameters (
P) and ends with a return type
Stop here for totality reasons even though the continuation ends with
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
type to make lives easier.
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
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 construction1.
Prog our EDSL within a
namespace to allow constructor name reuse2.
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
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
It’s next state is
Arg represents a parameter and as with
Pure it’s value must have the same type as specified by the
P constructor of
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.
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
This is how the ordering (sequenced using
Prog is dictated by
We provide implementations, as required, to
pure for Do-notation.
We can now construct a function
typeDef to dictate the initial and final states of a
typeDef uses the provided specification to
AType instance that represents the initial state with final value of
Stop, and we ask that our final state is
We finish with an example that uses
Append 4 3 Nat as a specification to type check against.
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.