The data type and decoder described by an IR code

An endo-code γ : IR I I denotes an endofunctor of Type/I, and the data type it describes is that endofunctor's initial algebra, carrying its decoder as the algebra's structure map into I — the µ γ and decode γ of [HancockMcBrideGhaniMalatestaAltenkirch2013], Section 3. It is obtained here from the translation IR.toSlicePFunctor of the code to a slice polynomial functor (Geb/Mathlib/Data/PFunctor/IndRec/Slice.lean) and the W-type of that functor (Geb/Mathlib/Data/PFunctor/Slice/W.lean). Routing through the translation is what makes the fixed point available at all: IR.interpObj computes by recursion on the code, so a data type defined directly as the fixed point of IR.interpObj γ would be rejected for the code variable γ, whereas SlicePFunctor.W is a subtype of an ordinary WType.

The algebra structure map — the constructor IR.W.mk, the in of Section 3 — needs a node of the direct interpretation to be presented as a node of the translated polynomial. That presentation is one direction of the agreement of the two semantics established by Lemma 2 of [HancockMcBrideGhaniMalatestaAltenkirch2013]. Its type mentions both semantics, so on its own it has no carrier to be folded into; it is computed instead as the third component of IR.posSlice, a fold whose other two components are the interpretation and the slice polynomial functor themselves.

Main definitions

IR.PosToSliceSig — the signature of the presentation of a node of an interpretation as a node of a slice polynomial functor.

IR.posToSliceIota, IR.posToSliceSigma, IR.posToSliceDelta — the per-shape steps of that presentation.

IR.PosSlice, IR.posSliceIota, IR.posSliceSigma, IR.posSliceDelta, IR.posSliceAlg, IR.posSlice — the three components folded together, the per-shape cases, the algebra assembling them, and the fold.

IR.W, IR.wDecode — the data type an endo-code describes and its decoder (µ γ and decode γ), with IR.wObj the object of Type/I they form.

IR.W.mk — the constructor, the in of Section 3.

Main statements

IR.posSlice_interp, IR.posSlice_spf — the first two components of IR.posSlice are IR.interpObj and IR.toSlicePFunctor.

IR.wDecode_mk — the decoder of a constructed element is the interpretation's decoding of the node it was constructed from: the algebra law of IR.W.mk.

Implementation notes

IR.W is stated for codes at IR.{max uA uI, uB, uI, uI}. The index universe must not exceed the code's arity universes: the objects of Type/I that IR.interpObj accepts have their carriers at Type (max uA uB), while the carrier of the W-type is at Type (max uA uB uI), so the two agree exactly when uI ≤ max uA uB.

IR.posSlice is a fold by IR.elim, whose computation rule is definitional, and not by the recursor IR.rec, whose computation rule is not. The difference is what lets everything built on it reduce on a closed code, so that a value equation about a concrete data type is rfl. It is bought by defining IR.W and IR.W.mk in terms of the fold's components rather than of IR.interpObj and IR.toSlicePFunctor, which IR.posSlice_interp and IR.posSlice_spf identify them with.

References

[HancockMcBrideGhaniMalatestaAltenkirch2013]

Tags

inductive-recursive, initial algebra, W-type, polynomial functor, slice category

The signature of the presentation of a node of an interpretation α as a node of a slice polynomial functor F, at the same output index: a node of α at an object X of Type/I yields a node of F at X whose shape-output index is the node's decoding.

The constant (iota) step of IR.posToSlice: the one shape of IR.toSlicePFunctorIota, with the empty direction assignment.

The dependent sum (sigma) step of IR.posToSlice: the node's arity element tags the subcode's shape into the coproduct of shapes.

The dependent product (delta) step of IR.posToSlice: the node's recursive fields become the directions of the representable factor of the summand at the assignment they induce, and the subcode's node the other factor.

The interpretation of a code, the code's slice polynomial functor, and the presentation of the former's nodes as the latter's, folded together. Folding the three together is what makes the presentation computable by IR.elim, whose computation rule is definitional, rather than by the recursor IR.rec, whose computation rule is not: the presentation's type mentions the other two components, so alone it has no fixed carrier.

The interpretation's object map.

The slice polynomial functor.

The presentation of an interpretation node as a functor node.

The constant (iota) case of IR.posSlice.

The dependent sum (sigma) case of IR.posSlice.

The dependent product (delta) case of IR.posSlice.

The algebra which computes one step of IR.posSlice.

A code's interpretation, slice polynomial functor, and the presentation of the former's nodes as the latter's — one direction of the agreement of the two semantics established by Lemma 2 of [HancockMcBrideGhaniMalatestaAltenkirch2013].

The interpretation component of IR.posSlice is IR.interpObj.

The functor component of IR.posSlice is IR.toSlicePFunctor.

The data type an endo-code describes (the µ γ of [HancockMcBrideGhaniMalatestaAltenkirch2013], Section 3): the W-type of the code's slice-polynomial translation.

The decoder of the data type an endo-code describes (the decode γ of [HancockMcBrideGhaniMalatestaAltenkirch2013], Section 3): the slice W-type's structure map.

The data type and its decoder read as an object of Type/I, the object at which the code's interpretation is taken to obtain the nodes IR.W.mk accepts.

The constructor of the data type an endo-code describes (the in of [HancockMcBrideGhaniMalatestaAltenkirch2013], Section 3): a node of the interpretation at IR.wObj, presented through IR.posSlice as a node of the translated polynomial. IR.posSlice_interp identifies the domain with IR.interpObj γ (IR.wObj I γ).

The decoder of a constructed element is the interpretation's decoding of the node it was constructed from: the algebra law of IR.W.mk.