The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-09-16 17:21 GMT+02:00 Daniel Schepler <dschepler AT gmail.com>:

On Tue, Sep 16, 2014 at 2:11 AM, Cedric Auger <sedrikov AT gmail.com> wrote:
> Yes, that is clever.
> By the way, I do not know why people use this definition of "fin" which I
> find rather inconvenient.
>
> Inductive emptySet : Type := .
>
> Fixpoint fin2 (n : nat) : Type := match n with O => emptySet | S n => option
> (fin2 n) end.
>
> is a lot more convenient from my point of view.
> Here, we do not have to do all these inversion stuff when inspecting an
> element.

I've often found that inductive versions have nicer extractions to
OCaml than the corresponding Fixpoint to Type or Set definitions whose
extractions require a lot of Obj.magic.
--
Daniel Schepler

Yes, you are right, I forgot about this.

Still, beware when passing a value of such an extracted type, as the indice is lost in the translation.
I mean, "fin" will be extracted to:

type fin = FinO | FinS of fin

and a function of type "fin 2 -> bool" will be extracted as a "fin -> bool", and thus could be passed "FinS (FinS (FinS (FinS FinO)))" as value although this does not make sense in the Coq world.

When I want to extract code to Ocaml, I often try to provide a "safe" interface, that is one for which all types are identically translated. This "fin" type (and even less the one I defined) would not appear in this interface (unless for functions using a "fin 1", "fin 2", … type which I can normalize as option… types, so translation to Ocaml is the identity).


--
.../Sedrikov\...