The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Thu, Dec 10, 2015 at 8:31 AM, Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk> wrote:

What are the theoretical reasons for not liking conductive types?

I don't know about theoretical reasons.  But practically, Coq's cofixpoint termination checker can be very limiting.  For example, the natural representation of a possibly non-terminating calculation would look like:

CoInductive calc (X:Type) : Type :=

| result : X

| step : calc X -> calc X.

This is naturally a monad with return := result and

CoFixpoint calc_bind {X:Type} (x:calc X) {Y:Type} (f:X->calc Y) : calc Y :=

match x with

| step x' => step (calc_bind x' f)

| result x0 => f x0

end.

For convenience:

Definition tick : calc unit :=

step (result tt).

(* Auger Cedric style notations *)

Notation "'do' x0 <- x ; y" := calc_bind x (fun x0 => y)

  (at level ?, right associativity, x0 ident).

Notation "'do' x >> y" := calc_bind x (fun _ => y)

  (at level ?, right associativity).

So far so good.  But now, try to represent the naive Fibonacci function as a naive user who doesn't know it will actually terminate:

CoFixpoint fib (n:nat) : calc nat :=

match n with

| 0 => result 0

| 1 => result 1

| S (S m) =>

  do Fm <- fib m;

  do tick >>

  do Fsm <- fib (S m);

  do tick >>

  result (Fm + Fsm)

end.

Coq won't accept this because of the occurrence of fib in the notation-produced function bodies (and I understand there are good reasons for rejecting such definitions).  In fact, I'm convinced that to produce a version that will be accepted, you'll essentially have to encode a runtime stack for the execution yourself - which isn't what you would have "signed up for" starting the exercise.

This example is due to Adam Chlipala.

-- 

Daniel Schepler