The goal of this lecture note is to describe how polymorphism is rendered and used in Gallina.
“morph” means “shape” and “poly” means “several” in Greek. So literally, something is polymorphic if it has several shapes. And likewise, something is monomorphic if it has one shape.
Gallina is a polymorphically typed programming language in that the type of an expression can contain type variables that are explicitly declared with a “forall” quantifier:
t ::= nat | bool | ... | t * t | t * ... * t | t -> t | ... | x | Type | forall x : Type, t | ...
So the type of the pairing function reads:
forall A : Type, forall B : Type, A -> B -> A * B
In practice, this type is syntactically sugared as:
forall (A : Type) (B : Type), A -> B -> A * B
So in Gallina, polymorphic types are parameterized types: the type variables are declared.
Here are several implementations of the pairing function, using an increasing amount of syntactic sugar:
Definition make_pair_v0 : forall (A : Type) (B : Type), A -> B -> A * B :=
fun (A : Type) (B : Type) (a : A) (b : B) => (a, b).
Definition make_pair_v1 (A : Type) : forall B : Type, A -> B -> A * B :=
fun (B : Type) (a : A) (b : B) => (a, b).
Definition make_pair_v2 (A : Type) (B : Type) : A -> B -> A * B :=
fun (a : A) (b : B) => (a, b).
Definition make_pair_v3 (A : Type) (B : Type) (a : A) : B -> A * B :=
fun (b : B) => (a, b).
Definition make_pair_v4 (A : Type) (B : Type) (a : A) (b : B) : A * B :=
(a, b).
So in Gallina, polymorphic functions are parameterized with a type.
Instantiating a type variable is achieved by applying a polymorphic function to that type. So for example tCPA processes Compute (make_pair_v4 nat bool 1 true). by emitting = (1, true) : nat * bool in the *response* window. Likewise for a function that duplicates its argument into a pair:
Definition duplicate (V : Type) (v : V) : V * V :=
make_pair_v4 V V v v.
Gallina also features polymorphic data types in that we can parameterize data-type declarations with type variables. For example, a polymorphic binary trees with payloads in the leaves is declared as follows:
Inductive polymorphic_binary_tree (V : Type) : Type :=
PLeaf : V -> polymorphic_binary_tree V
| PNode : polymorphic_binary_tree V -> polymorphic_binary_tree V -> polymorphic_binary_tree V.
Each constructor now is parameterized with a type.
This parameterization makes it possible—unlike in OCaml—to define polymorphic unit-test functions:
Definition test_number_of_leaves (candidate : forall V : Type, polymorphic_binary_tree V -> nat) :=
(candidate bool (PLeaf bool true) =? 1)
&&
(candidate nat (PNode nat (PLeaf nat 0) (PLeaf nat 1)) =? 2).
A function that processes a polymorphic binary tree is itself polymorphic. The match-expression that is used to dispatch on PLeaf and PNode requires us to put a placeholder for the type parameter. Otherwise, it is business as usual:
Fixpoint number_of_leaves (V : Type) (t : polymorphic_binary_tree V) : nat :=
match t with
PLeaf _ v =>
1
| PNode _ t1 t2 =>
number_of_leaves V t1 + number_of_leaves V t2
end.
To compare polymorphic binary trees, we parameterize the comparison function with a comparison function for its payloads:
Fixpoint eqb_polymorphic_binary_tree (V : Type) (eqb_V : V -> V -> bool) (t1 t2 : polymorphic_binary_tree V) : bool :=
match t1 with
PLeaf _ v1 =>
match t2 with
PLeaf _ v2 =>
eqb_V v1 v2
| PNode _ t11 t12 =>
false
end
| PNode _ t11 t12 =>
match t2 with
PLeaf _ v2 =>
false
| PNode _ t21 t22 =>
eqb_polymorphic_binary_tree V eqb_V t11 t21
&&
eqb_polymorphic_binary_tree V eqb_V t12 t22
end
end.
This comparison function is defined recursively on its first argument and by cases on its second argument.
Pablito: Structural equality?
Dana: “Structural” means “that follows the structure”.
Bong-sun: So eqb_polymorphic_binary_tree recursively tests whether the two given trees have the same structure...
Dana: ...and if they do, whether the payloads in the leaves are equal...
Pablito: ...using eqb_V, the given equality predicate at type V, I can see that, thanks.
Halcyon: Er... Shouldn’t we implement a unit-test function first?
Alfrothul: Indeed we should, Halcyon. Indeed we should. Do you want to implement one?
Halcyon (honestly): I am not completely sure how to do that.
Pablito: May I?
Halcyon: Please.
Pablito: First, we need to name it meaningfully. Here, meaningful means that its name is test_ followed by the name of the function we want to test:
Definition test_eqb_polymorphic_binary_tree ...
Halcyon: OK.
Pablito: Then, we parameterize it with the candidate function we want to test:
Definition test_eqb_polymorphic_binary_tree (candidate : forall V : Type, (V -> V -> bool) -> polymorphic_binary_tree V -> polymorphic_binary_tree V -> bool) : bool :=
...
Halcyon: And the result of the unit-test function is a boolean, OK.
Pablito: Right. Then, the body of the function is a conjunction of tests. For example, we can test whether applying the candidate function to two leaves with the same payload yields true:
Definition test_eqb_polymorphic_binary_tree (candidate : forall V : Type, (V -> V -> bool) -> polymorphic_binary_tree V -> polymorphic_binary_tree V -> bool) : bool :=
(Bool.eqb
(candidate
nat
Nat.eqb
(PLeaf nat 0)
(PLeaf nat 0))
true)
...
Halcyon: OK.
Pablito: We can also test whether applying the candidate function to two nodes that contain the same leaves also yields true:
Definition test_eqb_polymorphic_binary_tree (candidate : forall V : Type, (V -> V -> bool) -> polymorphic_binary_tree V -> polymorphic_binary_tree V -> bool) : bool :=
(Bool.eqb
(candidate
nat
Nat.eqb
(PLeaf nat 0)
(PLeaf nat 0))
true)
&&
(Bool.eqb
(candidate
nat
Nat.eqb
(PNode
nat
(PLeaf nat 0)
(PLeaf nat 0))
(PNode
nat
(PLeaf nat 0)
(PLeaf nat 0)))
true).
Pablito: It’s not a very good unit-test function, but you see its structure?
Halcyon: I see its structure, but why is it not a very good unit-test function?
Pablito: Because we can easily defeat it with a fake candidate function. For example, the constant candidate function that always returns true passes the tests, look:
Compute (test_eqb_polymorphic_binary_tree_easily_defeated
(fun (V : Type)
(eqb_V : V -> V -> bool)
(t1 t2 : polymorphic_binary_tree V) =>
true)).
Halcyon: Right – the *response* window reads:
= true
: bool
Pablito: So we need to also have negative tests in the conjunction.
Halcyon: Negative tests?
Pablito: Tests that not only check that the candidate function returns true when it should – these are positive tests, but also tests that check that the candidate function returns false when it should – these are negative tests. Let me add a negative test with two leaves that do not have the same payload:
Definition test_eqb_polymorphic_binary_tree (candidate : forall V : Type, (V -> V -> bool) -> polymorphic_binary_tree V -> polymorphic_binary_tree V -> bool) : bool :=
(Bool.eqb
(candidate
nat
Nat.eqb
(PLeaf nat 0)
(PLeaf nat 0))
true)
&&
(Bool.eqb
(candidate
nat
Nat.eqb
(PLeaf nat 0)
(PLeaf nat 1))
false)
&&
(Bool.eqb
(candidate
nat
Nat.eqb
(PNode
nat
(PLeaf nat 0)
(PLeaf nat 0))
(PNode
nat
(PLeaf nat 0)
(PLeaf nat 0)))
true).
Halcyon: Ah, OK.
Pablito: But we are not done yet.
Halcyon: We are not done?
Pablito: We are not.
Halcyon: Why are we not done?
Pablito: Because our unit tests must provide code coverage.
Halcyon: Code what?
Pablito: Coverage. Code coverage. All the conditional branches of the program should be evaluated when the unit-test function is applied.
Halcyon: And the unit-test function you just implement doesn’t provide code coverage?
Pablito: It doesn’t. For example, look at the clause in the base case:
match t2 with
PLeaf _ v2 =>
eqb_V v1 v2
| PNode _ t11 t12 =>
false
end
Pablito (continuing): The conditional branch false is not evaluated during the tests because the candidate function is not applied to a leaf and a node.
Bong-sun: May I be pedantic for a second?
Pablito: Sure.
Bong-sun: Suppose that the conditional branch eqb_V v1 v2 is written as a conditional expression:
match t2 with
PLeaf _ v2 =>
if eqb_V v1 v2
then true
else false
| PNode _ t11 t12 =>
false
end
Pablito: OK, that’s pedantic.
Bong-sun: It is, but it also makes it explicit that there are two conditional branches when both the given trees are leaves.
Pablito: True, that.
Bong-sun: And it also makes it clear that your unit tests provide code coverage there, since they both test the case where the two given trees are the same leaves and the case where the two given trees are not the same leaves.
Loki: So there is something to be said for being pedantic.
Bong-sun: Sometimes, yes.
Pablito: Anyway, we should also test the case where the candidate function is applied to a leaf and a node:
...
&&
(Bool.eqb
(candidate
nat
Nat.eqb
(PLeaf nat 0)
(PNode
nat
(PLeaf nat 1)
(PLeaf nat 2)))
false)
&&
...
Halcyon: I am guessing that we should also test the case where the candidate function is applied to a node and a leaf:
...
&&
(Bool.eqb
(candidate
nat
Nat.eqb
(PNode
nat
(PLeaf nat 1)
(PLeaf nat 2))
(PLeaf nat 0))
false)
&&
...
Pablito: Indeed we should, thanks.
Bong-sun: And then regarding the boolean conjunction in the induction step, there are four possibilities, so there should be four tests.
Halcyon: And then that’s it?
Pablito: Yes, that’s it: all the possibilities are covered in the unit-test function.
Mimer: Which is why “code coverage” is also referred to as “test coverage”.
In the resource file, complete test_eqb_polymorphic_binary_tree so that it provides code coverage for eqb_polymorphic_binary_tree, and recapitulate why it does.
Anton: Question.
Mimer: Yes, Anton?
Anton: My implementation of eqb_polymorphic_binary_tree is a lot simpler, look:
Fixpoint eqb_polymorphic_binary_tree' (V : Type) (eqb_V : V -> V -> bool) (t1 t2 : polymorphic_binary_tree V) : bool :=
match (t1, t2) with
(PLeaf _ v1, PLeaf _ v2) =>
eqb_V v1 v2
| (PNode _ t11 t12, PNode _ t21 t22) =>
eqb_polymorphic_binary_tree' V eqb_V t11 t21
&&
eqb_polymorphic_binary_tree' V eqb_V t12 t22
| _ =>
false
end.
Mimer: Indeed it it a lot shorter.
Anton: Simpler too, no?
Mimer: Well, prima facie it is less efficient.
Anton: Less efficient?
Mimer: Well, yes – at each call, an intermediate pair is constructed and then immediately deconstructed.
Anton: Well, I am trusting the compiler to optimize that away.
Mimer: But then what you see is not what you get, and the point here is to acquire a sense of reasoning about what we write.
Anton: Harrumph.
Mimer: And then there is the point of understanding what we program. In the declaration above, it is clear that the predicate is defined recursively over its first argument and by case on its second argument. But here, it looks like the predicate is defined recursively over both its arguments, which is a lot more complicated if that were to be the case.
Anton: On the other hand, my definition makes it simpler to enumerate all the possible cases to have code coverage in the unit-test function.
Mimer (diplomatic): That it might.
Anton: But I see your point.
Mimer: And you will see it even more in Week 03, when we start to reason about recursive functions over binary trees.
Anton: Looking forward to it.
For example, a function testing the structural equality of binary trees of natural numbers is obtained by instantiating eqb_polymorphic_binary_tree with the type of natural numbers and the equality predicate for natural numbers:
Definition eqb_nat := Nat.eqb.
Definition eqb_binary_tree_of_nats (t1 t2 : polymorphic_binary_tree nat) : bool :=
eqb_polymorphic_binary_tree nat eqb_nat t1 t2.
And a function testing the structural equality of binary trees of booleans is obtained by instantiating eqb_polymorphic_binary_tree with the type of booleans and the equality predicate for booleans:
Definition eqb_bool := Bool.eqb.
Definition eqb_binary_tree_of_bools (t1 t2 : polymorphic_binary_tree bools) : bool :=
eqb_polymorphic_binary_tree bool eqb_bool t1 t2.
Anton: This exercise is a straight followup of Exercise 05, isn’t it?Alfrothul: Looks like, Anton. Looks like.Pablito: So we need to implement several recursive functions?Alfrothul: Doesn’t look like, Pablito. Doesn’t look like.Pablito: How so?Anton: Well, look at the definitions of eqb_binary_tree_of_nats and of eqb_binary_tree_of_bools.
As in OCaml, the option type and its constructors Some and None exists in Gallina.
In the line of Section Structural equality of polymorphic binary trees,
implement a comparison function for optional values:
Definition eqb_option (V : Type) (eqb_V : V -> V -> bool) (ov1 ov2 : option V) : bool :=
...
implement a function testing the structural equality of optional binary trees of natural numbers:
Definition eqb_optional_binary_tree_of_nats (t1 t2 : option (polymorphic_binary_tree nat)) : bool :=
...
implement a function testing the structural equality of optional binary trees of optional natural numbers:
Definition eqb_optional_binary_tree_of_optional_nats (t1 t2 : option (polymorphic_binary_tree (option nat))) : bool :=
...
implement a function testing the structural equality of binary trees of optional binary trees of natural numbers:
Definition eqb_binary_tree_of_optional_binary_tree_of_nats (t1 t2 : polymorphic_binary_tree (option (polymorphic_binary_tree nat))) : bool :=
...
implement a function testing the structural equality of binary trees of optional binary trees of optional natural numbers:
Definition eqb_binary_tree_of_optional_binary_tree_of_optional_nats (t1 t2 : polymorphic_binary_tree (option (polymorphic_binary_tree (option nat)))) : bool :=
...
Bong-sun: Let’s see. The option type is a sum...
Dana: ...so the comparison function is defined by cases:
Definition eqb_option (V : Type) (eqb_V : V -> V -> bool) (ov1 ov2 : option V) : bool :=
match ov1 with
Some v1 =>
match ov2 with
Some v2 =>
...
| None =>
...
end
| None =>
match ov2 with
Some v =>
...
| None =>
...
end
end.
Pablito: When the two given arguments are not constructed with the same constructor, they are not equal:
Definition eqb_option (V : Type) (eqb_V : V -> V -> bool) (ov1 ov2 : option V) : bool :=
match ov1 with
Some v1 =>
match ov2 with
Some v2 =>
...
| None =>
false
end
| None =>
match ov2 with
Some v =>
false
| None =>
...
end
end.
Anton: And when they both are None, they are equal:
Definition eqb_option (V : Type) (eqb_V : V -> V -> bool) (ov1 ov2 : option V) : bool :=
match ov1 with
Some v1 =>
match ov2 with
Some v2 =>
...
| None =>
false
end
| None =>
match ov2 with
Some v =>
false
| None =>
true
end
end.
Halcyon: Which leaves us with the case where they are both constructed with Some.
Alfrothul: So if the first argument is Some v1 and if the second argument is Some v2, they are equal whenever v1 and v2 are equal. Luckily eqb_option is parameterized with the equality predicate eqb_V, so let’s use it:
Definition eqb_option (V : Type) (eqb_V : V -> V -> bool) (ov1 ov2 : option V) : bool :=
match ov1 with
Some v1 =>
match ov2 with
Some v2 =>
eqb_V v1 v2
| None =>
false
end
| None =>
match ov2 with
Some v =>
false
| None =>
true
end
end.
Mimer: Tadaa!
Dana: Now for implementing an equality predicate for optional binary trees of natural numbers... We are going to use eqb_option at type polymorphic_binary_tree nat.
Bong-sun (practical): Let’s see:
Check (eqb_option (polymorphic_binary_tree nat)).
Pablito (diligent): The *response* window reads:
eqb_option (polymorphic_binary_tree nat)
: (polymorphic_binary_tree nat -> polymorphic_binary_tree nat -> bool) ->
option (polymorphic_binary_tree nat) -> option (polymorphic_binary_tree nat) -> bool
Anton: Aha. So all we need is something of type polymorphic_binary_tree nat -> polymorphic_binary_tree nat -> bool.
Alfrothul: Presto:
Check (eqb_polymorphic_binary_tree nat eqb_nat).
Pablito (dutiful): The *response* window reads:
eqb_polymorphic_binary_tree nat eqb_nat
: polymorphic_binary_tree nat -> polymorphic_binary_tree nat -> bool
Bong-sun: So here we go:
Check (eqb_option (polymorphic_binary_tree nat) (eqb_polymorphic_binary_tree nat eqb_nat)).
Pablito (happily): The *response* window reads:
eqb_option (polymorphic_binary_tree nat) (eqb_polymorphic_binary_tree nat eqb_nat)
: option (polymorphic_binary_tree nat) -> option (polymorphic_binary_tree nat) -> bool
Dana: So we are done here:
Definition eqb_optional_binary_tree_of_nats (t1 t2 : option (polymorphic_binary_tree nat)) : bool :=
eqb_option (polymorphic_binary_tree nat) (eqb_polymorphic_binary_tree nat eqb_nat) t1 t2.
Halcyon: But we have defined eqb_binary_tree_of_nats already, haven’t we?
Dana: Well spotted, Halcyon:
Definition eqb_optional_binary_tree_of_nats' (t1 t2 : option (polymorphic_binary_tree nat)) : bool :=
eqb_option (polymorphic_binary_tree nat) eqb_binary_tree_of_nats t1 t2.
Bong-sun: Actually, we don’t need to declare t1 and t2, look:
Definition eqb_optional_binary_tree_of_nats'' : option (polymorphic_binary_tree nat) -> option (polymorphic_binary_tree nat) -> bool :=
eqb_option (polymorphic_binary_tree nat) eqb_binary_tree_of_nats.
Dana: Or we could just declare t1, look:
Definition eqb_optional_binary_tree_of_nats''' (t1 : option (polymorphic_binary_tree nat)) : option (polymorphic_binary_tree nat) -> bool :=
eqb_option (polymorphic_binary_tree nat) eqb_binary_tree_of_nats t1.
Alfrothul: The marvels of syntactic sugar:
Definition eqb_optional_binary_tree_of_nats'''' (t1 : option (polymorphic_binary_tree nat)) (t2 : option (polymorphic_binary_tree nat)) : bool :=
eqb_option (polymorphic_binary_tree nat) eqb_binary_tree_of_nats t1 t2.
Pablito: This is fun.
Halcyon: Yup.
Declare a polymorphic data type of binary trees with payloads in the nodes, implement a function that counts the nodes in a given tree, and test it using a unit-test function that features trees of different types. Implement also a function that tests the structural equality of two binary trees with payloads in the nodes.
Declare a polymorphic data type of binary trees with payloads both in the leaves and in the nodes, implement a function that computes the height of a given tree, and test it using a unit-test function that features trees of different types. Implement also a function that tests the structural equality of two binary trees with payloads both in the leaves and in the nodes.
Having to pass a type parameter to every polymorphic constructor and function tends to become tiresome after a while, and so tCPA features some magic to declare implicit parameters.
For example, the option type and its constructors Some and None pre-exist, and it is a polymorphic data type, in that, e.g., (Some 10, Some true) has type option nat * option bool.
On the other hand, if we were to declare our own option type, we would need to pass a type parameter to the constructors:
Inductive option' (V : Type) : Type :=
Some' : V -> option' V
| None' : option' V.
Namely, we would need to write, e.g., (Some' nat 10, Some' bool true), which has type option' nat * option' bool.
The reason for Some needing no type parameter is that the declaration of the option type, in the initial library, was preceded by:
Set Implicit Arguments.
For example, let us now declare:
Inductive option'' (V : Type) : Type :=
Some'' : V -> option'' V
| None'' : option'' V.
Since this declaration was preceded by Set Implicit Arguments., the type parameter is now implicit, and (Some'' 10, Some'' true) has type option nat * option bool: the type argument has been inferred from the context.
What about None, None', and None'' then? Here is what the Check command says:
(Incidentally, to specify that we are wish for an instance of None at a particular type, say, nat, we write (@None nat)).
Warning
Added the two interludes [14 Apr 2024]
Fixed a typo in the statement of Exercise 10 [19 Jan 2024]
Created [18 Jan 2024]