# 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.

```nix
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`.

```nix
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`.

```nix
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;
  };
```