Two challenges for dependently typed languages
September 23, 2014 - Tagged as: coq, en.
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
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
You may want to solve this simple exercise just to warm-up:
Now the challenge is to prove that cardinality of
) : Type
: T A
→ T A
→ T A
.. is 1 + N + N × N
is cardinality of A
UPDATE: First solution for this challange came from jrw
, in Coq: http://lpaste.net/111568
. UPDATE: He 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:
Extracted/executed version of pascal_nth
and any auxiliary function should be clean from type arguments.
Now the verification part:
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.