STLC Recursive Lists

Lists are already available in the HOAS layer as a generated recursive datatype. This surface gives them ordinary STLC syntax and shows how omitted element types can be solved from an expected List A.

List constructors

List A, nil A, and cons A h t translate to the generated HOAS list carrier and constructors.

list = elem: surface.mk "list" { inherit elem; };
nil = elem: surface.mk "nil" { inherit elem; };
cons = elem: head: tail: surface.mk "cons" { inherit elem head tail; };

explicitNilNat = nil H.nat;
oneTwoList =
  cons H.nat one
    (cons H.nat (H.natLit 2) explicitNilNat);

Folding lists

The fold form elaborates to listElim with a constant result type. The checked example computes the sum of [1, 1, 1] and proves the result is 3.

listFold = elem: result: onNil: onCons: scrut:
  surface.mk "listFold" { inherit elem result onNil onCons scrut; };

sumList = xs:
  listFold H.nat H.nat H.zero
    (head: _tail: ih: add head ih)
    xs;

stlcListFoldSumChecks =
  (H.checkHoas (H.eq H.nat (sumList ones) three) H.refl).tag == "desc-con";

Element-type holes

implicitNil and implicitCons allocate a surface metavariable for the missing element type. Checking against List Nat solves that metavariable as Nat.

implicitElementFromExpected = { context, label, hoas ? H }:
  let
    implicit = context.implicitMeta {
      type = { ctx = C.emptyCtx; ty = V.vU V.vLevelZero; };
      inherit label;
    };
    expectedType = context.expectedType or null;
    elem = if expectedType == null then null else listElement expectedType;
  in
  if expectedType == null
  then S.unsolvedImplicitError { metas = [{ id = implicit.id; }]; }
  else if elem == null
  then expectedListError context
  else {
    inherit elem implicit;
    solvedState = M.solveMeta implicit.id (E.eval [ ] (hoas.elab elem)) implicit.state;
  };