Two challenges for dependently typed languages

September 23, 2014 - Tagged as: coq, en.

Require Import Fin.
Require Import Arith.
Require Import Omega.
Require Import Program.

I propose two challenges that I think are very useful to see how easy to use a dependently typed language is. Different dependently typed languages use different type theories as their trusted cores and admit different axioms. In my experience, this significantly effects user experience. For example, lack of dependent pattern matching in Coq is leading to horribly verbose, hard to write, read and understand pattern matching code(see convoy and transport patterns).

Adding some extra axioms to Coq’s trusted but sometimes too simple core can make the experience significantly better(see JMec, Program and dependent destruction). On the other hand, languages like Idris handles some of the cases that Coq can’t handle by default.

The challenge is to solve two problems defined below in different dependently typed languages. We can then compare programs for 1) simplicity of code 2) use of extra axioms 3) giving away totality or some other useful properties.

Solutions of one of the challenges may also be compared for erasure of types. Problems are defined in Coq.

Challenge 1: Cardinality

This is a theorem proving exercise. Cardinality of a type is defined as bijection of the type with Fin.t n for some n:

Inductive cardinality (A : Type) (n : nat) : Prop :=
| cardinality_intro
    (to_fin    : A -> Fin.t n)
    (from_fin  : Fin.t n -> A)
    (bijection :
      (forall x, from_fin (to_fin x) = x) /\ (forall y, to_fin (from_fin y) = y)).

You may want to solve this simple exercise just to warm-up:

Theorem cardinality_bool : cardinality bool 2.
Admitted.

Now the challenge is to prove that cardinality of

Inductive T (A : Type) : Type :=
| T1 : T A
| T2 : A -> T A
| T3 : A -> A -> T A.

.. is 1 + N + N * N where N is cardinality of A:

Theorem cardinality_T : forall A N,
  cardinality A N -> cardinality (T A) (1 + N + N * N).
Admitted.

UPDATE: First solution for this challange came from jrw, in Coq. UPDATE: He also wrote an awesome blog post: Reasoning about Cardinalities of Sums and Products.

UPDATE 2: See comments for more solutions.

Challenge 2: Verified, CoInductive definition of Pascal’s Triangle

This should be easier. What’s good about this one is that we can compare languages for performance and/or erasure properties. Basically we expect type arguments to be absent in extracted/executed code.

Here’s one way to define the problem:

CoInductive triangle_t (T : Type) : nat -> Type :=
| triangle : forall (n : nat), Vector.t T n -> triangle_t T (S n) -> triangle_t T n.

Definition pascal : triangle_t nat 0. Admitted.

Definition pascal_nth (row col : nat) : col <= row -> nat. Admitted.

Extracted/executed version of [pascal_nth] and any auxiliary function should be clean from type arguments.

Now the verification part:

Theorem pascal_first_col_is_1 : forall row,
  pascal_nth row 0 (le_0_n row) = 1.
Admitted.

Theorem pascal_last_col_is_1 : forall n,
  pascal_nth n n (le_n n) = 1.
Admitted.

Lemma pascal_correct_aux : forall row col,
  col < row ->
  row >= 1 ->
  col >= 1 ->
  col - 1 <= row - 1.
Proof. intros. omega. Qed.

Lemma lt_le : forall a b,
  a < b -> a <= b.
Proof. intros. omega. Qed.

Lemma pascal_correct_aux' : forall row col,
  col < row ->
  row >= 1 ->
  col >= 1 ->
  col <= row - 1.
Proof. intros. omega. Qed.

Theorem pascal_correct : forall row col
  (pf : col < row)
  (pf_row : row >= 1)
  (pf_col : col >= 1),
  pascal_nth row col (lt_le col row pf) =
      pascal_nth (row - 1) (col - 1) (pascal_correct_aux row col pf pf_row pf_col)
    + pascal_nth (row - 1) col (pascal_correct_aux' row col pf pf_row pf_col).
Admitted.

Feel free to change the definitions. The point is to 1) have strict [nth] function that fail 2) prove that the data structure has property of Pascal’s triangle.

I’m hoping to come up with some solutions given in Coq over the next couple of weeks.

---