STLC Core Surface

This example builds a small source language over the existing HOAS checker. The surface adds syntax and source positions; the kernel still owns typing and normalization.

Define the surface

defineSurface maps each source constructor to a HOAS expression. The core STLC fragment has Pi types, lambdas, annotations, and applications.

surface = S.defineSurface {
  name = "STLC";
  description = "Small typed lambda-calculus surface example.";
  constructors = {
    lam = {
      tag = "stlc.lam";
      handler = { depth, h, elaborate, hoas, ... }:
        elaborate depth (hoas.lam h.name h.domain h.body);
    };

    app = {
      tag = "stlc.app";
      handler = { depth, h, elaborate, hoas, ... }:
        elaborate depth (hoas.app h.fn h.arg);
    };
  };
};

Smart constructors

Users construct source terms with small Nix functions. The values are surface nodes until check elaborates them into HOAS.

arrow = domain: codomain: pi "_" domain (_: codomain);
lam = name: domain: body: surface.mk "lam" { inherit name domain body; };
ann = term: type: surface.mk "ann" { inherit term type; };
app = fn: arg: surface.mk "app" { inherit fn arg; };

idNatTy = arrow H.nat H.nat;
idNat = lam "x" H.nat (x: var x);
idNatAnn = ann idNat idNatTy;

Expected-type holes

holeLam omits a lambda domain. The handler reads the expected type, solves a surface implicit metavariable with the Pi domain, and then elaborates an ordinary typed lambda.

holeLambdaFromExpected = { context, name, body, hoas ? H }:
  let
    implicit = context.implicitMeta {
      type = { ctx = C.emptyCtx; ty = V.vU V.vLevelZero; };
      label = "stlc.lambda-domain";
    };
    expectedType = context.expectedType or null;
    domain = if expectedType == null then null else piDomain expectedType;
  in
  if expectedType == null
  then S.unsolvedImplicitError { metas = [{ id = implicit.id; }]; }
  else if domain == null
  then expectedFunctionError context
  else {
    term = hoas.lam name domain body;
    solvedState = M.solveMeta implicit.id (E.eval [ ] (hoas.elab domain)) implicit.state;
  };

Implicit insertion

Plicity-style implicit binders are carried as sidecars on Pi and lambda nodes. During application, the elaborator inserts fresh metas for implicit arguments and solves them from explicit arguments or the expected residual type.

polyIdTy = implicitPi "A" universe0 (A: arrow A A);
polyId = implicitLam "A" universe0 (A: lam "x" A (x: var x));
polyIdAnn = ann polyId polyIdTy;

stlcPolyIdAppliedSolvesImplicit =
  let
    position = { path = [ "poly" "id" "zero" ]; };
    r = check (app polyIdAnn H.zero) H.nat position;
  in
  !(r ? error) && r.tag == "app";