The Coq mailing list

[C T McBride <c.t.mcbride AT durham.ac.uk>]

Hello all

Subject to `size of type' restrictions, it is possible to turn
inductive-recursive definitions into inductive families. That is,
an inductive-recursive type with a decoder

  T : Type
  d : T -> D

becomes a family indexed by its decoding

  F : D -> Type

Let's have an example. Apologies in advance for making the syntax up as I
go along...

For a suitable X, with distinctness predicate #,

  DList : Type
  fresh : DList -> X -> Prop

  dnil : DList
  dcons : (x:X)(xs:DList)(p:fresh xs x)DList

  fresh dnil y = True
  fresh (dcons x xs p) y = ((x # y) /\ (fresh xs y)

becomes

  DList : (X -> Prop) -> Type

  dnil : DList ([y:X]True)
  dcons : (x:X)(fresh_xs:X->Prop)(xs:DList fresh_xs)(p:fresh_xs x)
          (DList ([y:X](x # y) /\ (fresh_xs x)))

More generally, for each constructor c,

 (1) replace recursive arguments (t:T) by
       decoding-argument pairs (d_t:D)(t:F d)
       i.e. make the constructor polymorphic in the decoding of its
       recursive arguments
 (2) correspondingly, replace applications of the decoder (d t) by the new
       `decoding argument' d_t
 (3) construct the index of the return type from the c-case of the decoder
       i.e. replace the return type by (F d_c),
         where d_c is [d_t / (d t)]rhs
         where the original decoding function has
               d (c ...) = rhs

You can now take

  T = Sigma d : D. (F d)

and decode by first projection.

Now, if I remember rightly, the usual rules for inductive families
suggest that F must occupy at least as big a universe as D, which may
interfere with some uses of induction-recursion for universe
constructions. Also, if you have higher-order recursive arguments, then
their `decoding arguments' must also be lambda-lifted, which may cause
annoying technical difficulties in systems without eta-laws for function
spaces. But for simple examples like DList it works ok.

I don't pretend that this is pretty, but if you haven't got
induction-recursion, then it may be worth considering this fake.

Hope this helps

Conor