This post has an accompanying github repo.
Intro
Haskell’s type system has long been sort of a lab rat for experiments on many concepts relevant to type theory. Especially lately there has been quite a lot of interest in typelevel programming and dependent types.
What initially piqued my interest in trying to use Haskell to prove mathematical theorems at the type level was a blog post called “Proving stuff in Haskell” by Mads Buch. It is quite fun to follow so I’m not going to go into detail, but the gist is to use propositional equality to prove a theorem by showing that two haskell types are actually the same type. So for example, if we wanted to prove that \(a + b = b + a\) (commutativity of addition of natural numbers) then we’ll have a function whose type reflects exactly that property, rather than using actual values to prove it (more on that later).
Writing proofs using the type system is nothing new. What I describe in this post is first of all a way to write readable proofs by induction using the same steps we would use if the proof was done on paper, and then how to actually use these proofs to “nudge” the type system to compile code that could not be compiled otherwise.
One disclaimer: I am definitely not an expert so many things might
not be correct. This post’s style is informal and more of a braindump,
much like some of my favourite posts out there.
If you find any errors or if you have any question or comment, feel free
to drop me an email (alexpeitsinis [at] gmail [dot] com
) or
find me at fpslack (@alexpeits
). What follows is also most
definitely not suitable for “production use”. However I believe it’s a
good application of using dependent types and some more exotic language
extensions.
Setting up
Unless I am completely mistaken, code should compile along the way. Here are the required language extensions:
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
I’ll also try to note why and when an extension should be enabled.
Dependent types
I’ve already given some spoilers, so here it is: to achieve what we want to do I’m going to use whatever Haskell offers to simulate a dependently typed language. To better understand the what and how of dependent types, I suggest taking a look at any work by Richard Eisenberg, especially the extremely well written Stitch functional pearl (Eisenberg 2020). Another great resource for everything typelevel related is the book “Thinking with Types” by Sandy Maguire (consider buying it, it’s awesome). Finally, the Idris language tutorial is a great resource, especially to understand what needs to be done differently in Haskell and how.
Many of the following do not require dependent types and can probably be modeled using e.g. type classes, but I’m going to use dependent types here.
Natural numbers
To prove theorems on natural number operations we first need a way to represent natural numbers at the type level. The canonical way to do this is to use Peano numbers:
data Nat = Z  S Nat
We have the base case which is the number zero (here Z
for brevity later), and then we recursively define the successor
(S
). So to represent the number 1 we would write
S Z
(at the type level), to represent the number 2 we would
write S (S Z)
and so on. The thing is, we’d not use the
value Z
or S Z
, because they
have the same type, Nat
, which is not very useful for
typelevel programming. On the other hand, because the types
Z
and S Z
have kind Nat
and not
*
, they cannot have any inhabitants, meaning that there is
no value x
so that x :: Z
or
x :: S Z
. But there is a way to circumvent that
restriction, which will be described later.
In the above explanation we can use Z
and S
as types thanks to the DataKinds
extension. What it does is
“promote” data constructors to types and types to kinds. One thing to
note is that there is no way to get a value of one of those types, as
their kinds is Nat
and not *
. We could also
have written something like this:
data Z
data S a
What we lose from this definition is the way to unite those two types
under a kind. Our definition allows writing Nat
in GADT and
type family declarations, which adds a layer of type safety. Otherwise
we’d have to use *
, which, in some cases, would allow for
illformed types.
Type equality
There is a ridiculously simple way to convince the type system that two types are equal using propositional equality in the module Data.Type.Equality.
data a :~: b where
Refl :: a :~: a
What this means is that, if somewhere in our code we have the type
a :~: b
and somehow manage to give it the value
Refl
, we have convinced the type checker that types
a
and b
are exactly the same, which is exactly
what we want to achieve in our proofs.
Typelevel functions
In order to actually have something to prove, we’ll define addition at the type level as per the Peano axiom for addition.
\[ \begin{align} a + 0 = a && \text{(1)}\\ a + S(b) = S (a + b) && \text{(2)}\\ \end{align} \]
This can be achieved using a closed type family:
type family a + b where
a + Z = a  (1)
a + S b = S (a + b)  (2)
(from now on I’ll refer to those two properties as (1)
and (2)
respectively)
We don’t need to specify a kind for this type family explicitly, as
it is deduced to be Nat > Nat > Nat
since the type
family is closed (no more instances can be defined). Also, the symbol
+
does not clash with the addition function, for the same
reason the type Z
does not clash with the value
Z
(if there is an ambiguity in that case we can tell the
type system that we’re talking about the type Z
by
writing 'Z
).
First proof
Now let’s try to combine this type family definition with propositional equality:
testEquality :: (Z + Z) :~: Z
testEquality = Refl
This type checks because Refl
says “ok, I need
Z + Z
to be the same as Z
. But when the type
checker sees Z + Z
, it uses (1)
to say that
Z + Z = Z
, where a = Z
, and our equality
stands. This is the first proof! The fact that we don’t need to give any
values or”nudge” the type system in any way means that the elaboration
happens automatically, and this equality stands every time. Let’s also
try not with concrete types, but with a type variable:
testEquality' :: (a + Z) :~: a
testEquality' = Refl
This type checks, again thanks to (1)
. Let’s try
(2)
:
testEquality'' :: (a + S b) :~: S (a + b)
testEquality'' = Refl
And yet again, this type checks, this time thanks to
(2)
. Now let’s try something that is not immediately
apparent. With testEquality'
, we proved the right identity
property of addition. What about left identity?
plusLeftId :: (Z + a) :~: a
plusLeftId = Refl
Which, when compiled, unfortunately fails:
• Couldn't match type ‘a’ with ‘'Z + a’
‘a’ is a rigid type variable bound by
the type signature for:
plusLeftId :: forall (a :: Nat). ('Z + a) :~: a
at ...
Expected type: ('Z + a) :~: a
Actual type: a :~: a
• In the expression: Refl
In an equation for ‘plusLeftId’: plusLeftId = Refl
• Relevant bindings include
plusLeftId :: ('Z + a) :~: a
(bound at ...)

70  plusLeftId = Refl
 ^^^^
However simple it seems, the type checker knows nothing about natural
number addition, so we have to convince it that this is indeed correct.
To prove that Z + a = a
we need to do induction on
a
. By induction, I mean that we need to prove a base case,
then assume that our hypothesis holds for \(a\) and prove that it holds for \(S (a)\). If we prove that, we have proven
the theorem for all natural numbers. That’s because if we substitute
\(a\) for Z
then our
hypothesis holds because we’ve already proven for Z
. So if
we manage to prove for S Z
, then we do the same for
S (S Z)
and so on. We could try something like this:
baseCase :: (Z + Z) :~: Z
baseCase = Refl
induction :: (Z + S a) :~: S a
induction = ???
But we find a dead end. We need to be able to use one proof in order to prove another one.
Long story short, looking in Data.Type.Equality
again,
there is a function that seems like it does exactly that: gcastWith.
gcastWith :: (a :~: b) > (a ~ b => r) > r
In simple terms, what gCastWith
says is: give me a
Refl
that proves a
is the same type as
b
, and something of type r
that could use the
knowledge that a
is b
, and I will tell your
type checker that r
is well typed. This seems like the same
logic used in one step of a mathematical proof. So we could do things
like:
helper :: (S Z + S Z) :~: S (S Z + Z)
helper = Refl
stupid :: (S Z + S Z) :~: S (S Z)
stupid = gcastWith helper Refl
What this says is: “I know that S Z + S Z
is
S (S Z + Z)
, now use that”. Then the Refl
in
stupid
says “ok, I have S Z + S Z
and the
other guy says that this is S (S Z + Z)
, can I use it? Ah,
of course, from (1)
I know that S Z + Z
is
S Z
, so what I have is S (S Z)
, that’s it!”
(or as mathematicians say, Q.E.D.). OK, to be fair
this is not necessary as stupid
is proven directly: it’s 2
reduction steps of the +
type family.
Still, we are talking about concrete values, whereas what we need to
prove has a type variable a
. We need to somehow recurse
until we reach the base case, which means we’ll need to reflect the
exact type we have in the signature of
plusLeftId
to a value. If you peeked at the Idris tutorial,
you might say something like
{a:Nat} > (Z + S a) :~: S a
. There is a way to do this
in Haskell, using singletons.
Singletons
Singletons, as their name implies, are values that have a 11 mapping
with their relevant types. This means that, when we have a singleton
value v
of type T
then we know for sure that
v
always has the type T
(that makes sense),
but also that type T
has only one inhabitant (only one
possible value), and that is v
. This is the singleton
definition for our Nat
:
data SNat :: Nat > * where
SZ :: SNat Z
SS :: SNat a > SNat (S a)
Now, if we ask for the type of SZ
we get
SNat Z
, and SS (SS (SZ))
gives
SNat (S (S Z))
. It goes without saying that we cannot write
SS (SS (SZ)) :: SNat Z
or something similar, because that
gets rejected by the definition of the SNat
GADT.
Revisiting the proof
Let’s try to prove left identity again, this time using an
SNat
to help us with the induction by allowing
recursion:
plusLeftId :: SNat a > (Z + a) :~: a
The base case will be for a ~ Z
(~
is type
equality):
plusLeftId :: SNat a > (Z + a) :~: a
plusLeftId SZ = Refl
This type checks because, according to the Refl
value,
(Z + Z) ~ Z
which is true from (1)
. The reason
that a
is assumed to be Z
is that the first
parameter is SZ :: SNat Z
, so a ~ Z
. That’s
very similar to the type signature in Idris:
{a:Nat} > (Z + S a) :~: S a
, only with some indirection
via the singleton type for Nat
!
Now for the induction step. Recall that we need to now prove for
every type S a
, assuming that the proof stands for
a
. So we’ll use the singleton for the successor,
SS
:
plusLeftId :: SNat a > (Z + a) :~: a
plusLeftId SZ = Refl
plusLeftId (SS n) = Refl
But this fails:
• Could not deduce: ('Z + n) ~ n
from the context: m ~ 'S n
bound by a pattern with constructor:
SS :: forall (m :: Nat). SNat m > SNat ('S m),
in an equation for ‘plusLeftId’
(I have made the error message a bit more readable)
Which makes sense: we have to tell the type checker that the
equality holds for n
. So, as described earlier, we’ll use
gcastWith
:
plusLeftId :: SNat a > (Z + a) :~: a
plusLeftId SZ = Refl
plusLeftId (SS n) = gcastWith ??? Refl
Recall that
gcastWith :: (a :~: b) > (a ~ b => r) > r
. Here,
Refl
is the r
, and, according to the error
message, we need a ~ (Z + n)
and b ~ n
, or
even better (Z + n) :~: n
. But that’s the result type of
plusLeftId
itself, if we called it with n
:
plusLeftId :: SNat a > (Z + a) :~: a
plusLeftId SZ = Refl
plusLeftId (SS n) = gcastWith (plusLeftId n) Refl
And it type checks (try calling the function with any
SNat
value)!
Let’s also rewrite the proof for right identity, as well as the axioms we automatically get from the type family, to use values:
given1 :: SNat a > (a + Z) :~: a
given1 _ = Refl
given2 :: SNat a > SNat b > (a + S b) :~: S (a + b)
given2 _ _ = Refl
plusRightId :: SNat a > (a + Z) :~: a
plusRightId = given1
Of course the first two don’t need anything further to be proved. The
same applies for right identity, but here I used given1
to
demonstrate the use of a proof in another proof. This would work
too:
plusRightId' :: SNat a > (a + Z) :~: a
plusRightId' n = gcastWith (given1 n) Refl
Proofs with multiple steps
The proof for left identity was a relatively simple one. Here it is in mathematical notation, copied from here. (I’ll refer to the addition axiom as \((1)\) and \((2)\)):
\[ \begin{align} & 0 + S(a)\\ =\ & S(0 + a) && \text{by (2)}\\ =\ & S(a) && \text{by the induction hypothesis}\\ \end{align} \]
This means that in the proof we went from Z + (S n)
to
S (Z + n)
by using the type family definition, and then
proved what’s inside the S
inductively. It makes sense that
we want to work on Z + n
, since the error we first got said
exactly that:
• Could not deduce: ('Z + n) ~ n
from the context: m ~ 'S n
Proving the associativity of addition
Let’s now try a proof that’s a bit more complex: associativity of addition. So we’ll prove that \((a + b) + c = a + (b + c)\). I am going to copy the mathematical notation for the proof here and follow that verbatim, rather than explaining each step.
For the base case c = 0:
\[ \begin{align} & (a + b) + 0\\ =\ & a + b && \text{by (1) for}\ a + b\\ =\ & a + (b + 0) && \text{by (1) for}\ b\\ \end{align} \]
For the induction, assuming \((a + b) + c = a + (b + c)\):
\[ \begin{align} & (a + b) + S(c)\\ =\ & S((a + b) + c) && \text{by (2)}\\ =\ & S(a + (b + c)) && \text{by the induction hypothesis}\\ =\ & a + S(b + c) && \text{by (2)}\\ =\ & a + (b + S(c)) && \text{by (2)}\\ \end{align} \]
Let’s try to prove that in Haskell. First I’m going to take the long
path and not assume that (1)
and (2)
are
resolved automatically. This will help build some groundwork for later
proofs. This will not typecheck for now so I’m going to use undefined in
several places, but the intermediate steps are correct and correspond
11 with the steps above. Let’s also define addition for the singleton
datatype, which will be useful because its type can directly reflect to
the +
type family:
(!+) :: SNat n > SNat m > SNat (n + m)
n !+ SZ = n
n !+ (SS m) = SS (n !+ m)
We’ll use this function to construct, for example, the \(a + b\) in the base case of the proof given \(a\) and \(b\). Here it goes:
plusAssoc
:: SNat a
> SNat b
> SNat c
> ((a + b) + c) :~: (a + (b + c))
plusAssoc a b SZ =
let
step1 :: SNat x > SNat y > ((x + y) + Z) :~: (x + y)
step1 x y = gcastWith (given1 (x !+ y)) Refl  (1)
step2 :: SNat x > SNat y > (x + y) :~: (x + (y + Z))
step2 x y = gcastWith (given1 y) Refl  (1)
in undefined
What we do in those 2 steps is exactly what we do in the base case
for \(c = 0\). I used x
and y
to make it clear that we’re not talking about
a
and b
, but just defining steps based on two
numbers, even though we’re going to pass a
and
b
in those methods. In the first step, just as in the first
step of the proof, we want to say that
((x + y) + Z) ~ (x + y)
. It’s the first time we’ve seen a
more complex argument in the proofs so far. Given that we need to use
(1)
to prove this, we have to pass something of type
SNat n
where n is of type x + y
. That’s why
the addition for singletons (!+
) is used here. The
resulting type of this addition, if we pass in x :: x
and
y :: y
is x + y
. The second step is a bit
easier to understand. The main trick here is to extract the
part of the expression that we want to “transform” to something
else, and then use another proof function to drive the process.
It’s clear what needs to be done now. We want the type
((a + b) + Z) :~: (a + (b + Z))
, and we have the types (I
substitute x
and y
for a
and
b
for clarity) ((a + b) + Z) :~: (a + b)
and
(a + b) :~: (a + (b + Z))
. Fortunately, this is like saying
“if type x is the same as type y, and type y is the same as type z, then
is type x the same as type z”? Of course it is! Let’s prove it (I’ll
also use a fancy symbol to make the process clearer later):
(==>) :: a :~: b > b :~: c > a :~: c
Refl ==> Refl = Refl
Since the above type checks, the proof stands. This is the
transitive property of :~:
(propositional
equality).
Let’s see how this helps:
plusAssoc
:: SNat a
> SNat b
> SNat c
> ((a + b) + c) :~: (a + (b + c))
plusAssoc a b SZ =
let
step1 :: SNat x > SNat y > ((x + y) + Z) :~: (x + y)
step1 x y = gcastWith (given1 (x !+ y)) Refl  (1)
step2 :: SNat x > SNat y > (x + y) :~: (x + (y + Z))
step2 x y = gcastWith (given1 y) Refl  (1)
in step1 a b ==> step2 a b
Voilà! Onward to the next step, the induction.
plusAssoc
:: SNat a
> SNat b
> SNat c
> ((a + b) + c) :~: (a + (b + c))
plusAssoc a b SZ = ...
plusAssoc a b (SS c) =
let
step1
:: SNat x > SNat y > SNat (S z) > ((x + y) + S z) :~: S ((x + y) + z)
step1 x y (SS z) = gcastWith (given2 (x !+ y) (SS z)) Refl  (2)
step2
:: SNat x > SNat y > SNat z > S ((x + y) + z) :~: S (x + (y + z))
step2 x y z = gcastWith (plusAssoc x y z) Refl  induction
step3
:: SNat x > SNat y > SNat z > S (x + (y + z)) :~: (x + S (y + z))
step3 x y z = gcastWith (given2 x (y !+ z)) Refl  (2)
step4
:: SNat x > SNat y > SNat z > (x + S (y + z)) :~: (x + (y + S z))
step4 x y z = gcastWith (given2 y z) Refl  (2)
in step1 a b (SS c) ==> step2 a b c ==> step3 a b c ==> step4 a b c
To be fair, none of this is needed for both stages of the proof.
Since all but the induction step are inferred automatically by the
+
type family, the proof can be written more compactly:
plusAssoc
:: SNat a
> SNat b
> SNat c
> ((a + b) + c) :~: (a + (b + c))
plusAssoc a b SZ = Refl
plusAssoc a b (SS c) = gcastWith (plusAssoc a b c) Refl
In this case, only the induction step is needed to help the second step typecheck. But the long proof shows a lot on how to take a mathematical proof and directly apply it in Haskell.
Bonus: using ScopedTypeVariables
we can make it much
prettier. We’ll use a forall
in the let
block
to bring some fresh variables in scope, and define the steps inside it,
using the same names in the types so that we don’t have to pass
variables to each step:
plusAssoc
:: SNat a
> SNat b
> SNat c
> ((a + b) + c) :~: (a + (b + c))
plusAssoc a b SZ =
let proof :: forall x y. SNat x > SNat y > ((x + y) + Z) :~: (x + (y + Z))
proof x y = step1 ==> step2
where
step1 :: ((x + y) + Z) :~: (x + y)
step1 = gcastWith (given1 (x !+ y)) Refl
step2 :: (x + y) :~: (x + (y + Z))
step2 = gcastWith (given1 y) Refl
in proof a b
plusAssoc a b (SS c) =
let proof ::
forall x y z.
SNat x > SNat y > SNat z >
((x + y) + S z) :~: (x + (y + S z))
proof x y z = step1 ==> step2 ==> step3 ==> step4
where
step1 :: ((x + y) + S z) :~: S ((x + y) + z)
step1 = gcastWith (given2 (x !+ y) (SS z)) Refl
step2 :: S ((x + y) + z) :~: S (x + (y + z))
step2 = gcastWith (plusAssoc x y z) Refl
step3 :: S (x + (y + z)) :~: (x + S (y + z))
step3 = gcastWith (given2 x (y !+ z)) Refl
step4 :: (x + S (y + z)) :~: (x + (y + S z))
step4 = gcastWith (given2 y z) Refl
in proof a b c
Commutativity
Here’s the proof (in mathematical notation) for the property of commutativity of addition. What we want to prove is \(a + b = b + a\):
The base case \(b = 0\) is the left identity property.
For the second base case \(b = 1\):
 First we prove it for \(a = 0\), which gives \(0 + 1 = 1 + 0\), the right identity property.
 Then we prove inductively, assuming \(a + 1 = 1 + a\):
\[ \begin{align} & S(a) + 1\\ =\ & S(a) + S(0) && \text{by definition of natural numbers}\\ =\ & S(S(a) + 0) && \text{by (2)}\\ =\ & S((a + 1) + 0) && \text{by definition of natural numbers}\\ =\ & S(a + 1) && \text{as proved by the base case for}\ b = 0 \\ =\ & S(1 + a) && \text{by the induction hypothesis}\\ =\ & 1 + S(a) && \text{by (2)}\\ \end{align} \]
For the induction, assuming \(a + b = b + a\):
\[ \begin{align} & a + S(b)\\ =\ & a + (b + 1) && \text{by definition of natural numbers}\\ =\ & (a + b) + 1 && \text{by associativity}\\ =\ & (b + a) + 1 && \text{by the induction hypothesis}\\ =\ & b + (a + 1) && \text{by associativity}\\ =\ & b + (1 + a) && \text{by the base case for}\ b = 1 \\ =\ & (b + 1) + a && \text{by associativity}\\ =\ & S(b) + a && \text{by definition of natural numbers}\\ \end{align} \]
The proof is left as an exercise, but using the same pattern as in the associativity proof it should be pretty straightforward. The signature should be:
plusComm :: SNat a > SNat b > (a + b) :~: (b + a)
The proof (and even more proofs) can be found in the repo.
Using the proofs
It was a bit difficult to find a use case for the proofs on addition, but I quickly found an issue trying to append two lengthindexed vectors. The vector definition and several operations are more or less the same as the ones in the Stitch paper:
data Vec :: Nat > * > * where
V0 :: Vec Z a
(:>) :: a > Vec n a > Vec (S n) a
infixr 5 :>
I’m not going to go into detail here, but the most important part is that this vector type has its length in its type as extra information, and we need to reason about the length when manipulating it.
One common example is appending two vectors. It is apparent that if
one has length n
and the other has length m
,
then the resulting vector will have length n + m
. A naive
first attempt would be the following:
append :: Vec n a > Vec m a > Vec (n + m) a
append V0 ys = ys
append (x:>xs) ys = undefined  let's wait for now
But even the base case fails to typecheck:
• Could not deduce: ('Z + m) ~ m
from the context: n ~ 'Z
The error says that the only concrete information we have is
n ~ Z
, because the first vector is the empty vector. And
because we return ys
, which has length m
, the
resulting type Z + m
should be the same as m
,
but the type checker is not convinced. Let’s notice that what we need is
to use the left identity property, and convince the checker:
append :: Vec n a > Vec m a > Vec (n + m) a
append V0 ys = gcastWith (plusLeftId ?) ys
append (x:>xs) ys = undefined  let's wait for now
There is one important part missing: the actual length. All our proofs used singletons to help drive the checking process, but here there is no mention of a singleton. So let’s add it for now, and later we’ll try to make this process implicit. We’ll explicitly pass the lengths of both vectors:
append :: SNat n > SNat m > Vec n a > Vec m a > Vec (n + m) a
append SZ m V0 ys = gcastWith (plusLeftId m) ys
append n m (x:>xs) ys = undefined  let's wait for now
OK, this works. Let’s try to do the next case where the first vector is nonempty. We’ll make it fail just to see the error message:
append :: SNat n > SNat m > Vec n a > Vec m a > Vec (n + m) a
append SZ m V0 ys = gcastWith (plusLeftId m) ys
append n m (x:>xs) ys = x :> append ? m xs ys
Uhoh. How do we get the length of the first vector after we remove
the first element? Luckily, that’s just n  1
. Let’s create
a helper function to get the predecessor number of a singleton
of Nat
:
spred :: SNat (S n) > SNat n
spred (SS n) = n
This function is total, because there is no need for the case
spred SZ
. As a matter of fact, it wouldn’t type check
because it would mean trying to do SZ :: SNat (S n)
which
doesn’t make sense. And because the first vector in the second case of
append
is not empty, we know that n
is not
SZ
but SS ...
.
append :: SNat n > SNat m > Vec n a > Vec m a > Vec (n + m) a
append SZ m V0 ys = gcastWith (plusLeftId m) ys
append n m (x:>xs) ys = x :> append (spred n) m xs ys
This time we get this error:
• Could not deduce: ('S n1 + m) ~ 'S (n1 + m)
from the context: n ~ 'S n1
Where n1
is the type of the result of
spred n
. Let’s construct a proof for that:
We need to prove \(S(a) + b = S(a + b)\). We can do an inductive proof which will be quicker (in the repo I use an inductive proof), but let’s try to do it in one pass:
\[ \begin{align} & S(a) + b\\ =\ & b + S(a) && \text{by commutativity}\\ =\ & S(b + a) && \text{by (2)}\\ =\ & S(a + b) && \text{by commutativity}\\ \end{align} \]
And in Haskell:
append :: SNat n > SNat m > Vec n a > Vec m a > Vec (n + m) a
append SZ m V0 ys
= gcastWith (plusIdenL m) ys
append n m (x:>xs) ys
= gcastWith (proof pn m) $ x :> app (spred n) m xs ys
where
pn = spred n
proof :: forall x y. SNat x > SNat y > (S x + y) :~: S (x + y)
proof x y = step1 ==> step2 ==> step3
where
step1 :: (S x + y) :~: (y + S x)
step1 = gcastWith (plusComm (SS x) y) Refl
step2 :: (y + S x) :~: S (y + x)
step2 = gcastWith (given2 y (SS x)) Refl
step3 :: S (y + x) :~: S (x + y)
step3 = gcastWith (plusComm y x) Refl
And that’s the proof. Now appending two vectors should work. First,
here’s an instance of Show
for Vec
:
instance (Show a) => Show (Vec n a) where
show v = "[" ++ go v
where
go :: (Show a') => Vec n' a' > String
go v = case v of
V0 > "]"
(x :> xs) > show x ++ sep ++ go xs
where
sep = case xs of
V0 > ""
_ > ", "
And two example vectors:
x = 1 :> 2 :> 3 :> 4 :> V0
lengthX = SS (SS (SS (SS SZ)))
y = 5 :> 6 :> 7 :> 8 :> 9 :> V0
lengthY = SS (SS (SS (SS (SS SZ))))
> append lengthX lengthY x y
[1, 2, 3, 4, 5, 6, 7, 8, 9]
> :t append lengthX lengthY x y
append lengthX lengthY x y
:: Vec ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) Integer
We can also remove the need to have the length in a variable
beforehand. To do that, we have to resort to type classes (again, this
is described in the Stitch paper). We will construct a type class with a
single method that can magically give an SNat
depending on
the instance we are using:
class IsNat (n :: Nat) where nat :: SNat n
instance IsNat Z where
nat = SZ
instance IsNat n => IsNat (S n) where
nat = SS nat
Then we can just use nat
to get the length. The instance
of IsNat
to use is resolved thanks to the fact that the
n
in the constraint IsNat
is the same
n
that is the vector length:
vlength :: IsNat n => Vec n a > SNat n
vlength _ = nat
> append (vlength x) (vlength y) x y
[1, 2, 3, 4, 5, 6, 7, 8, 9]
But I promised that we can have the length passed implicitly. Again,
we’ll use the typeclass with some help from
TypeApplications
and ScopedTypeVariables
:
(+++) :: forall n m a. (IsNat n, IsNat m)
=> Vec n a
> Vec m a
> Vec (n + m) a
(+++) = append (nat @n) (nat @m)
> x +++ y
[1, 2, 3, 4, 5, 6, 7, 8, 9]
Magic!
Conclusion
This was a lengthy blog post, and the ideas presented fall into the obscure side of things. Should there be a need to resort to dependent types, the above might prove useful. Nevertheless, it’s a fun way to explore both dependent types and translating mathematical proofs to Haskell. After all, as someone said in the functional programming slack,
A relatively large number of people making zygosynchroid semiapplicative plesiofunctors, one madman pushing the type system to its limits, and like three people concerning themselves with practical software engineering using Haskell.