You may have heard of dependent types from the functional programming community. You may have heard that it has great advantages but it's hard to do.
In this post, I show some advantages with a few examples of dependent types to get you started on programming in dependent types.
To understand this post, it's best if you have some experience with functional programming and algebraic and recursive datatypes.
To understand dependent types, let's take a step back and review what types are.
From Programming in Martin-LΓΆf's Type Theory:
"Intuitively, a type is a collection of objects together with an equivalence relation. Examples of types are the type of sets, the type of elements in a set, the type of propositions, ...the type of predicates over a given set."
Don't worry if it's still not intuitive to you. We'll look at some of these examples in detail.
"To know that A
is a set is to know how to form the canonical elements in the set and under what conditions two canonical elements are equal."
Canonical elements are evaluated expressions or values.
In a universe of small types, which contains all types except itself, the type of sets is called Type
(or sometimes Set
). Elements of Type
include the type of natural numbers, the type of booleans, etc.
What are propositions? "To know that A
is a proposition is to know that A
is a set." That is, propositions are types! This leads to an important feature/advantage of dependent types: types can depend on propositions!
What does it mean for a proposition to be true? "To know that the proposition A
is true is to have an element a
in A
."
For example, from Idris's documentation onePlusOne
below is a proposition of the equality type, the only constructor it has is Refl
, which stands for reflexivity.
onePlusOne : 1+1=2
onePlusOne = Refl
Thus, the only way to construct the onePlusOne
type is via the Refl
constructor, which we can only use if the left and right hand sides of the equality sign evaluate to the same thing.
A dependent type is a type whose definition depends on a value. The classic example is Vector A n
, which is a list
of type A
with a specified length n
. The Vector
type depends on a natural number (the value).
In a dependently typed language, types are first class. That is, types can be arguments to a function, types can be returned, etc.
Vector A n
is both polymorphic and dependent. It's polymorphic because it can take any type A
. It's dependent because its output type depends on a value n
.
Here I present a definition of datatype that allows for dependent types. It's similar to Agda's.
In a universe of small types, we declare a datatype D
, of type π© β Type
, as follows:
data D (pβ : Pβ) ... (pβ : Pβ) : π© β Type
cβ : π«β β D pβ ... pβ tβΒΉ ... tβΒΉ
...
cβ : π«β β D pβ ... pβ tβα΅ ... tβα΅
That's a lot of symbols! Let's go through them in detail:
D
is the name of the datatype.:
is read as "is of type". E.g., pβ : Pβ
should be read as pβ
is of type Pβ
.D
takes in two types of inputs: parameters and indices. Parameters are the same for all constructors, indices can vary from constructor to constructor.pβ ... pβ
are parameters of D
. They are declared after the name of the datatype.D
are of types π©
.cβ ... cβ
are constructors of D
. The i-th constructor takes arguments π«α΅’
and have the return types D pβ ...pβ tββ± ... tββ±
where tββ± ... tββ±
are the arguments of the indices of D
.In the following sections I illustrate some example datatypes in this context.
The datatype of natural numbers can be introduced by:
data Nat : Type
zero : Nat
suc : Nat β Nat
Nat
is a datatype of type Type
. It has no parameter (there is no p
). It is not indexed (π©
is empty).
zero
is a constructor (cβ
) of Nat
. It doesn't take any argument (π«β
is empty). Its type is Nat
.
suc
is another constructor (cβ
) of Nat
. It takes a Nat
as an argument (π«β = Nat
). Its return type is Nat
.
The datatype family of lists is parameterised by A
, without being indexed:
data List (A : Type) : Type
nil : List A
cons : A β List A β List A
Lists are a type family because it is parameterised by a type (A
). That is, we can have many types in this family. For example, a member of the type family of lists is a list of integers ([Int]
in Haskell.)
List
is a datatype of type Type
. It has one parameter, pβ = A
. The type of the parameter is Type
, so Pβ = Type
.
It is not indexed (π©
is empty).
nil
is a constructor (cβ
) of List
. It doesn't take any argument (π«β
is empty). Its type is List A
.
cons
is another constructor (cβ
) of List
. It takes two arguments, π«β = A, List A
. Its return type is List A
.
The datatype family of vectors is parameterised by A
, indexed by the length of the list:
data Vec (A :Type) : Nat β Type
vnil : Vec A zero
vcons : {n : Nat} β A β Vec A n β Vec A (suc n)
Vec
is a datatype of type Nat β Type
. It has one parameter, pβ = A
. The type of the parameter is Type
, so Pβ = Type
.
It is indexed by a Nat
, so π©
= Nat
.
vnil
is a constructor (cβ
) of Vec
. It doesn't take any argument (π«β
is empty). Its type is Vec A zero
, so tβΒΉ = zero
.
vcons
is another constructor (cβ
) of Vec
. It takes 2 arguments, π«β = A, Vec A n
(the type of n
is specified by the implicit argument to be Nat
). Its return type is Vec A (suc n)
, so tβΒ² = suc n
.
The family of identity type can be defined by
data Id (A : Type) (x : A) : A β Type
refl : Id A x x
Id
is a datatype of type A β Type
. It has two parameters, pβ = A
, pβ = x
. The types of the parameters are Type
and A
, so Pβ = Type
, Pβ = A
.
It is indexed by x
of type A
, so π© = A
.
refl
is a constructor (cβ
) of Id
. It doesn't take any argument (π«β
is empty). Its type is Id A x x
, so tβΒΉ = x
.
Even
Dependent types can also be used to describe predicates. For example the predicate of even numbers, Even : Nat β Type
, can be defined as follows:
data Even : Nat β Type where
even-zero : Even zero
even-plus2 : {n : Nat} β Even n β Even (suc (suc n))
Even
is a datatype of type Nat β Type
. It has no parameter.
It is indexed by a Nat
, so π© = Nat
.
even-zero
is a constructor (cβ
) of Even
. It doesn't take any argument (π«β
is empty). Its type is Even zero
, so tβΒΉ = zero
.
even-plus2
is another constructor (cβ
) of Even
. It takes an argument Even n
(the type of n
is specified by the implicit argument to be Nat
) (π«β = Even n
). Its type is Even (suc (suc n))
, so tβΒ² = (suc (suc n))
.
To construct Even
, the index has to either be
zero
, in which case we can construct Even zero
with even-zero
,suc (suc n)
such that Even n
can be constructed. Using that Even n
and even-plus2
, we can construct Even (suc (suc n))
. Therefore, it has to be two = (suc (suc zero))
or (suc (suc two))
and so on.We've learned that dependent types allow us to define more intricate types using parameters and indices. They also allow us to construct predicates and proofs. I hope you enjoyed it. Cheers.
Marty Stumpf
Software engineer. Loves FP Haskell Coq Agda PLT. Always learning. Prior: Economist. Vegan, WOC in solidarity with POC.
See other articles by Marty
Ground Floor, Verse Building, 18 Brunswick Place, London, N1 6DZ
108 E 16th Street, New York, NY 10003
Join over 111,000 others and get access to exclusive content, job opportunities and more!