Enum := data {} where <nil@[]> <cons(u : UId; E : @ [])@[]> @[]
Sig := data {} where <nil@[]> <cons(u : UId; S : *; Sg : S → @ [])@[]> @[]
Data := \I : Sig => data {} where
<out(i : sig I)@[]>
<arg(u : UId; A : *; D : A → @[])@[]>
<rec(u : UId; i : sig I; D : @[])@[]>
<hrec(u : UId; H : *; i : H → sig I; D : @[])@[]>
@[]
These apparently meaningless scrawlings have just been eaten. Only by the parser, so far, but the right terms did seem to emerge from the other side. If I tell you that @ stands as a placeholder for the type being recursively defined by data, and that if Σ : Sig is a code, then sig Σ is the corresponding signature type, you might almost be able to tell that they are the datatypes Enum, Sig and Data I, of codes for enumerations, signatures and datatypes indexed by signature I, respectively. The relevant codes emerge successfully from the parser. Terribly circular, at the moment, but quite stratifiable.
Randy did something like this years ago, as a way of explaining the schemas to students. He even wrote LEGO programs to calculate the type of the induction principle and the two sides of the computation rules. Peter and I figured out how we could use a similar technique to deliver inductive datatypes and their elimination behaviour for real. You need just a few hardwired generic programs to calculate the type and behaviour of the elim rule.
Nicolas has very nearly made it all go. Epigram 2 core is coming alive!