Sources to "Another implementation of λ_Π".

LamPi.lidr

> module Micro
> import Data.String

Another implementation of λ_Π
=============================

An implementation of the dependently-typed language λ_Π in Idris - up to (but not including) a REPL, since Idris lacks quick support for parsing. You should be able to follow it if
- you have read "A tutorial implementation of a dependently typed lambda calculus", and now understand how to use a dependently-typed language, if not implement it;
- you can write a Scheme metacircular interpreter;
- understand how to write the usual suspects in an expressive type system like Idris';
- and you know how to follow semantic rules given in "natural deduction" style (and understand the basic premise of of specifying semantics: the correspondence between of given rules - "constraints" is better - and an actual procedure deciding well-typedness is less than straightforward.)

It is written, in terms of concepts, from the bottom up: Idris requires definition before use. You might prefer to read this in reverse order: in terms of concepts, top-down; in terms of the text, end-to-beginning. You might find quite a few concepts "razored" out from a conventional  metacircular interpreter, either way.

If you've read "A tutorial implementation[...]"
-----------------------------------------------

λ_Π is specified in "A tutorial implementation of a dependently typed lambda calculus" by Löh et al.; although the interpreter here is different in spirit. We'll deal with the differences here - the rest of the text shouldn't require close familiarity with the reference interpreter's implementation.

Unlike the original reference interpreter:

- Our abstract syntax representation is a one-to-one translation of that given with the semantics (rather than the reference interpreter) in the original paper. All terms are in Term.

- Our `eval` allows applications to all terms; undefined applications are caught by the typechecker. That's not to say that they'll evaluate to anything other than yet another App.

- As a consequence of the single Term type, the type checker does kind checking.

- As a consequence of the single Term type, we don't implement the guarantee that terms will evaluate to a "terminal" subset.

That's not to say that this isn't a useful guarantee: the only thing Terminal doesn't have that Term *does* have is Ann. But there are many other ways we can partition Term that we would like use, too -

- `infer` would like to statically declare the sets of terms it'll return, and terms that don't. (It won't return Ann or Lam, for example.)

- `infer` might also like to statically declare the sets of terms whose types we can only check, versus terms whose types we can infer.

Abstract syntax
---------------

> Name : Type
> Name = String

> data Term = Ann Term Term
>           | Star
>           | Pi Name Term Term
> -- "Arrow kinds and arrow types are subsumed by the new construct for the dependent function space."
>           | Vari Name
> -- "Type variables and term variables now coincide."
>           | App Term Term
>           | Lam Name Term

> Eq Term where
>   (Ann x y) == (Ann x' y') = (x == x') && (y == y')
>   Star == Star = True
>   (Pi x y z) == (Pi x' y' z') = (x == x') && (y == y') && (z == z')
>   (Vari x) == (Vari x') = x == x'
>   (App x y) == (App x' y') = (x == x') && (y == y')
>   (Lam x y) == (Lam x' y') = (x == x') && (y == y')
>   _ == _ = False

> Show Term where
>   show (Ann x y) = "(Ann " ++ (show x) ++ " " ++ (show y) ++ ")"
>   show Star = "Star"
>   show (Pi x y z) =
>     "(Pi " ++ (show x) ++ " " ++ (show y) ++ " "  ++ (show z) ++ ")"
>   show (Vari x) = "(Vari " ++ (show x) ++ ")"
>   show (App x y) = "(App " ++ (show x) ++ " " ++ (show y) ++ ")"
>   show (Lam x y) = "(Lam " ++ (show x) ++ " " ++ (show y) ++ ")"

Terms and types are irrevocably fused - there is only one Var; and splitting a "data Type" away from "data Term" would introduce two vars that *should* be equivalent for all intents and purposes... but by definition, aren't.

Environments
------------

A teaser in advance if you've written a Scheme interpreter before: "environments", although typed in the way you'd expect, aren't actualy used in λ_Π for variable bindings. To see what they're actually used for, examine the typechecker - the functions "assert" and "infer" - below.

> Env : Type
> Env = List (Name, Term)

> emptyEnv : Env
> emptyEnv = []

> unscope : Env -> Maybe Env
> unscope [] = Nothing
> unscope (x::xs) = Just xs

> scope : Env -> Name -> Term -> Env
> scope binds name binding = (name, binding)::binds

> get : Env -> Name -> Maybe Term
> get [] _ = Nothing
> get ((name', binding)::binds) name =
>   if name == name'
>     then Just binding
>     else get binds name

Env is a stack of bindings; since types are terms, the term "binding" includes typings.

If we were to use our stack of bindings for variable bindings, you'd be prudent to think that this might limit us to dynamic scoping - but there's a wrinkle in λ_Π that "closes" over free variables without carrying around an environment. It looks vaguely like
```
      e `evalsTo` v
-------------------------- (E-Lam)
λ.x → e `evalsTo` λ.x → v

(From Figure 8: Evaluation in λ_Π)
```
and specifies that, when an λ abstraction (and not an application) is evaluated, the abstracted-over term is evaluated - replacing variables with their bindings. We get away with early binding because λ_Π has no notion of variable mutation; a variable evaluated now is exactly the same as a variable evaluated later. Not that this is necessary for evaluation during the typechecking phase - Agda doesn't do it, for example: see "Agda does not evaluate expressions under lambdas[...]" in "The Utrecht Agda Compiler" by Hausmann et al.

(This is related to the fact that a precursor system to λ_Π - λ_→, is "strongly normalising" - "evaluation terminates for any term, independent of the evaluation strategy." λ_→ includes this evaluation rule, and the strongly normalising property should justify it if you read "evaluation terminates" to include "evaluation will not halt with unbound variable conditions", and "evaluation strategy" to include "closing over λ abstractions early".)

eval and apply
--------------

...although we've renamed `apply` to `subst`, to emphasise the fact that we're doing a purely syntactic operation here.

Substitution goes first.

> subst : Name -> Term -> Term -> Term
> subst name rep Star = Star
> subst name rep (Vari name') =
>   if name' == name then rep else Vari name'
> subst name rep (Ann term ty) = Ann (subst name rep term) ty
> subst name rep (App abs term) = App (subst name rep abs) (subst name rep term)
> -- The cases below deal with forms that introduce another
> -- binding. See [Rebinding] below.
> subst name rep (Lam name' term) =
>   if name' /= name
>     then Lam name' (subst name rep term)
>     else Lam name' term
> subst name rep (Pi name' ty term) =
>   if name /= name'
> -- ...although Pi has an exception to the above; see [Pi].
>     then Pi name' (subst name rep ty) (subst name rep term)
>     else Pi name' (subst name rep ty) term

**[Rebinding]:** We don't replace variables that are rebound within a λ or a Π abstraction; that is, `(λx.λx.x)γ 'evalsTo' λx.x`. This is straightforward, but isn't in fact given in the semantics (Figure 8, "Evaluation in λ_Π") - we're simply told to "substitute for the bound variable":
```
e 'evalsTo' λx → v    v[x ↦ e′] 'evalsTo' v′
--------------------------------------------
            e e′ 'evalsTo' v′
```

**[Pi]:** in `∀x:τ.τ′`, though, we do substitute into τ. The gritty details of substitution, again, aren't given in the semantics. With luck this is a reasonable exception-to-an-exception.
You'll notice `eval` doesn't have many reasons to go wrong - it simply refuses to evaluate. In effect, we're representing runtime errors by unevaluated terms. Why shouldn't our typechecker catch them, then?

Evaluation follows.

> eval : Term -> Term
> eval Star  = Star
> eval (Vari name) = Vari name
>   -- All Varis at this point are free; by definition, we cannot
>   -- meaningfully find a value to substitute for them.
>   -- For more, see the explanation below in addition to [Vari].
> eval (Ann term ty) = term
> eval (Lam var term) = Lam var (eval term)  -- See [Lam].
> eval (Pi var ty term) =
>   Pi var (eval ty) (eval term)  -- See [Pi].
> eval (App abs term) = case (eval abs) of
>   Lam var body => eval (subst var term body)
>          --  If you've read the notes below, you'll see why this
>          --  case is fairly significant. See [App.]
>   notLam => (App notLam term)

See Figure 8, "Evaluation in λ_Π".

Note that an implicit assumption in most metacircular interpreters - that all terms must evaluate to "simpler" terms or fail - doesn't hold here: when we can evaluate an App, we leave it untouched; when we can't find a binding for a Vari, we leave it untouched. The fact that `eval` returns a meaningful value given incomplete information - when variables in a Pi are unbound, for example - is what makes evaluation during type-checking meaningful. (Consider the case where a value extracted from an IO action is bound in a dependent type, for example: we must still be able to type-check without knowing what the value is.)

This simplicity includes the "razoring" out of variable binding environments: `eval` does not take variable bindings. In a metacircular interpreter for Scheme, environments implement the semantics of λ_Π, including the phenomena of binding during application and closure. But so does an executable description of the semantics itself, described only in terms of substitution! This is what we do here:

* Variables bound during application; the semantics has a rule for this. See [Lam].
* Variables occurring free, but bound in some global environment: we substitute early. Admittedly this is a pain when debugging.
* Closed-over environments; the semantics also has a rule for this. See [Lam].

**[Vari]:** If the variable *was* bound, substitution should have been done before: when recursing down a larger Term. App, for example, does substitution.

**[Lam]:** Remember (as explained in the description of Env) that, in `Lam var (eval term)`, the `eval term` is where closure is done; we don't evaluate Lam to anything "structurally" simpler.

**[Pi]:** Like λ abstractions, the result term is no "simpler". We don't do closing-over here.

**[App]:** Our substitution and Scheme's `apply` are implementations of the same thing: what the semantics describes as . An interesting parallel: when type-checking, we have to do an analogous operation of substituting into the "body" of a Pi.

assert and infer
----------------

We place this after eval and apply. Two reasons:

- We'd like to convince you that evaluation is straightforwards The extensions to evaluation - evaluating types of types is an intuitive extension to the evaluation of terms.

- In λ_Π, typing involves evaluation - but not vice-versa. (How is our typing a form of assurance, though, if typing in turn relies on untypechecked evaluation?)

> data CanInfer : Term -> Type where
>  CanInferStar : CanInfer Star
>  CanInferAnn : CanInfer (Ann t ty)
>  CanInferPi : CanInfer (Pi var ty body)
>  CanInferVari : CanInfer (Vari name)
>  CanInferApp : CanInfer (App l r)

> canInfer : (a : Term) -> Maybe (CanInfer a)
> canInfer (Lam _ _) = Nothing
> canInfer Star = Just CanInferStar
> canInfer (Ann _ _) = Just CanInferAnn
> canInfer (Pi _ _ _) = Just CanInferPi
> canInfer (Vari _) = Just CanInferVari
> canInfer (App _ _) = Just CanInferApp

The proposition "can this term's type be inferred?", and a decision procedure for it. (That is, can the term's type be reconstructed without peeking at any top-level annotations?) This partitions Term into two subsets. While λ_Π isn't designed to infer types for λ abstractions in general, it can easily do so for the other types - and, like in other expressively typed languages, we won't expect you to supply types.

(There are a few minor design choices that don't seem well-decided. Should the witness be implicit, or the term itself? Should the witness be "auto implicit" - Idris' term - equivalently, an "instance argument" - Agda's terminology? A good thing to wish for would be an idiomatic way of representing (and demonstrating) membership in mutually-exclusive subsets.)

Here's one way of representing things that don't seem fruitful.

- By giving the subset of all type-inferrable terms first, and then combining them into the parent set into Term. I haven't chosen to do so: I haven't found a way of doing so that the type checker can verify.

- Defining the type CantInfer, and using some form of the excluded middle to get "can infer".

> Checking : Type -> Type
> Checking = Either String

> fail : {a: Type} -> String -> Checking a
> fail = Left

> succeed : {a: Type} -> a -> Checking a
> succeed = Right

> mustHold : Bool -> String -> Checking ()
> mustHold test err = if test then succeed () else fail err

The common infrastructure for our typechecker - we want to describe the processes of typechecking as a series of constraints: note that either has >>= defined. So our type-checking is written declaratively, claiming that certain equations must hold - as in `mustHold`. From `mustHold` we build up larger constraint declarations.

> assert : Term -> Term -> Env -> Checking ()
> infer : (term : Term) -> {wit : CanInfer term} -> Env -> Checking Term

The typechecker is `assert`; the type inferrer is `infer`. Both rely on   each other: the type checker, by λ_Π's specification, must assert that type inference (when possible) must give results equivalent to annotated types (when given). The type inferrer must, also by definition, assert that τ : *, where τ is any term whose use is as a type. (What are the semantics of `foo : 3`, for example?)

> assert term ty ctx with (canInfer term)
>   assert term ty ctx           | (Just wit) = do
>     inferredTy <- infer term {wit} ctx
>     mustHold (inferredTy == ty) "The type we've inferred doesn't match the type you've given us; this is, by λ_Π's definition, an error. You gave us {this}; we inferred {this}."
>   assert (Lam var term) ty ctx | Nothing = case ty of
>       (Pi pi_var pi_var_ty pi_term_ty) =>
>         assert term pi_term_ty
>           (scope (scope ctx var pi_var_ty)
>             pi_var pi_var_ty)
>         -- If you've read the original λ_Π paper, convince yourself
>         -- that we don't need to substitute for de Bruijn indices, and
>         -- that we have to type *both* bound variables in the context.
>       otherwise => fail ("A λ must have the type of the form {looks like this}. You gave us {this.}")

Typechecking involves either (a) matching inferred types with given types, or (b) if we can't infer types, simply checking for "internal consistency".

(The `with` syntax is fairly nice: it collapse smultiple case analyses into a signle concise expression. I do think equations are a natural and general way to express pattern constraints and pattern matching. But Idris has poorly spelt-out rules on how far the | must be indented.

But even better would be to see the tests in the order they're done, and the dependent patterns after the test. Here, the canInfer check is last, even though the patterns `(Lam ...)` require that it must be true.)

> infer Star ctx = Right Star -- Yes, Star : Star. See [Star].
> infer (Vari name) ctx = case (get ctx name) of
>   Just ty => Right ty
>   Nothing => do
>     fail "The variable {variable} has not been given a type."
> infer (Ann term ty) ctx = do
>   assert ty Star ctx
>   let normalised_ty = eval ty
>     -- Dependent typechecking involves evaluation.
>   assert term normalised_ty ctx
>   succeed normalised_ty
> infer (Pi var var_ty body_ty) ctx = do
>   assert var_ty Star ctx
>   let normalised_var_ty = eval var_ty
>   assert body_ty Star (scope ctx var normalised_var_ty)
>   succeed Star
> infer (App abs arg) ctx with (canInfer abs)
>   infer (App abs arg) ctx | Nothing =
>     fail "A naked λ-abstraction can't be applied. I suggest annotating it."
> -- You might think this case analysis rules out
> -- (App (Lam ...) ...) - which seems to be *the* canonical
> -- form of an application. It does, but we're not in fact
> -- applying naked Lams - see [App] below.
>   infer (App abs arg) ctx | (Just wit) = do
>     abs_ty <- infer abs {wit} ctx
>     case abs_ty of
>      Pi dep_var arg_ty res_ty => do
>        assert arg arg_ty ctx
>        succeed (eval (subst dep_var arg res_ty))
>        -- And at this crucial point the Pi's variable is bound,
>        -- and evaluation is done on the type; see [AppPi].
>      otherwise => fail "A term of type {type} cannot be applied to any term; by λ_Π's definition, only terms of the form {forall} can be applied."

Inference - as you might think would be intuitive - recurses on the syntax. The base cases are atomic terms with known types - variables, types themselves. As we've seen above, though, there is no "inductive step" for Lam.

**[Star]:** As the authors of λ_Π reference implementation note: * : * renders the type system inconsistent; Girard's paradox is a construction that the typing rules will both claim is valid and not. (And what about our typecheckers?)

**[App]:** In `infer abs ctx`, you might think we're asking for the inferred type of a Lam - but in fact we aren't: we're asking for the inferred type of a Lam within an Ann. That we don't have ensure Lams are annotated through syntactic measures is a fairly sweet thing.

**[AppPi]:** It's worth repeating the note above: our questions on how terms are introduced into types are answered here; so are our questions on how types are evaluated. Note that our ability to evaluate applications with unbound variables back to the same applications is crucial - in general, a treatment of unbound variables is required for evaluation when typechecking. We repeat that note as well where relevant.

The core of a REPL
------------------

The language proper ends here; what follows are utilities and definitions for a REPL.

> substEnv : Env -> Term -> Term
> substEnv [] term = term
> substEnv ((l, r)::binds) term = substEnv binds (subst l r term)

Substitutes all the bindings in an Env into a Term. Why do we need this? Briefly - to implement a top-level "let" expression. Peek down under `substCheckEvalAnn` for more.

> annotated : Term -> Env -> Checking Term
> annotated term ctx with (canInfer term)
>   annotated term ctx | Nothing = succeed term
>   annotated term ctx | Just wit = do
>     type <- infer term ctx {wit}
>     succeed (Ann term type)

The REPL tries to annotate resulting terms with their types whenever they can be inferred; this isn't always possible.

> substCheckEvalAnn : Term -> Env -> Env -> Checking Term
> substCheckEvalAnn (Ann term ty) ptys pdefs =
>   let term' = substEnv pdefs term
>       ty' = substEnv pdefs ty
>   in do
>     assert term' ty' ptys
>     annotated (eval term') ptys
> substCheckEvalAnn term ptys pdefs =
>   let term' = substEnv pdefs term
>   in case (canInfer term') of
>     Nothing => do
>       fail "Your term {term} can't be typechecked. You've tried to evaluate a term that isn't annotated with a type, and whose type can't be inferred."
>     Just wit => do
>       ty' <- infer term' ptys {wit}
>       assert term' ty' ptys
>         -- assert will likely call "infer" again - but that's
>         -- solely an internal concern.
>       annotated (eval term') ptys

(We said Checking was written to be used declaratively. That understanding's a bit stretched here. Regrets? I've had a few.)

`substCheckEvalAnn` is an important, self-contained chunk of a REPL's functionality: it takes a term to evaluate, along with an Env of type assertions and an Env of predefined variables to substitute in; typechecks it; evaluates it; annotates it with a type, if inference is possible; and returns this annotated term for printing.

Notice the use of an Env for bindings. we weren't kidding when we said that λ_Π only needed Envs for typechecking. The REPL language, on the other hand, might extend λ_Π with the ability to define - and rededefine - variables at the top-level scope, for the sake of incrementally working. But this doesn't effect eval, substitute, and friends - our assumptions of immutability during the evaluation of a term, used above to perform (the equivalent of) closure, remain unaffected. Here, we use the same immutability assumption to "early bind" variables. (See [Lam] under the implementation of `eval` for a justification of both.)

When done, checkEvalAnnotate don't need to return updated typings and bindings.

Not a REPL, but a language extension
------------------------------------

We adopt the point of view that the REPL has a language of its own - a straightforward extension to λ_Π. Like λ_Π, it is expression-oriented, and it is strongly typed. Unlike λ_Π, though, it has one side-effecting inclusion: an expression that binds a variable, and evalutes to the bound value. (That the REPL takes nothing more - or less - than terms in a language is a Scheme idiom.)

That being said, we don't have parsing facilities easily available. We'll cheap out and define a non-interactive interpreter for our REPL language.
Unlike λ_Π, its `eval` always returns the equivalent of an Ann.

> data ReplTerm = Define Name Term Term
>               | Lift Term

Remember that λ-abstractions evaluate with the evaluation of their bodies - unbound variables and all.

Now define an interpreter for single ReplTerms, and build on top an interpreter for non-empty lists of ReplTerms.

> replTermEval : ReplTerm -> Env -> Env -> Checking (Term, Env, Env)
> replTermEval (Lift term) ptys pdefs = do
>   term' <- substCheckEvalAnn term ptys pdefs
>   succeed (term', ptys, pdefs)
> replTermEval (Define name term ty) ptys pdefs = do
>   term' <- substCheckEvalAnn (Ann term ty) ptys pdefs
>   ty' <- substCheckEvalAnn ty ptys pdefs
>   let pdefs' = (name, (Ann term' ty'))::pdefs
>   succeed (term', ptys, pdefs')

> replEvalInner : (a : List ReplTerm) -> Env -> Env -> {auto wit: NonEmpty a} -> Checking Term
> replEvalInner [] _ _ {wit = IsNonEmpty} impossible
> replEvalInner (x::xs) ptys pdefs with (nonEmpty xs)
>   replEvalInner (x::[]) ptys pdefs | No = do
>     (finalTerm, _, _) <- replTermEval x ptys pdefs
>     succeed finalTerm
>   replEvalInner (x::xs) ptys pdefs | Yes wit = do
>     (_, ptys', pdefs') <- replTermEval x ptys pdefs
>     replEvalInner xs ptys' pdefs' {wit = wit}

> replEval :  (a : List ReplTerm) -> {auto wit: NonEmpty a} -> Checking Term
> replEval [] {wit = IsNonEmpty} impossible
> replEval rTerms = replEvalInner rTerms emptyEnv emptyEnv

Note the use of the `with` syntax again in `replEvalInner`: given a nonempty list of the form `(x:xs)`, we'd do a case analysis on `xs`: is it empty, or is it not? An equivalent way of expressing this would be to "lower" this down into the body of the definition.

Our handiwork
-------------

The evaluation of types is straightforward - it's easy to introduce atomic types with the type of *, after all.

- Star evaluates to itself, and is its own type:

```
Idris> substCheckEvalAnn Star emptyEnv emptyEnv
Right (Ann Star Star)
```

```
Idris> substCheckEvalAnn (Ann (Vari "x") (Vari "x")) [] [("x", Star)]
Right (Ann Star Star)
```

- A Pi has type Star, and, like a Lam, evaluates to its own closure.
```
Idris> substCheckEvalAnn (Pi "x" Star (Vari "y")) [("y", Star)] [("y", Star)]
Right Ann (Pi "x" Star Star) Star
```

- We can give a variable a type without having to define it; this is not only well-defined, but is exactly what allows evaluation before runtime.

```
Idris> substCheckEvalAnn (Vari "Bottom") [("Bottom", Star)] []
Right (Ann (Vari "Bottom") Star)
```

Now on to terms - excluding application, for now.

- This is `id_*`; that is, `id` defined on types. The core of our REPL cannot infer a type for the value; it still remains typechecked.

```
Idris> substCheckEvalAnn (Ann (Lam "x" (Vari "x")) (Pi "x" Star Star)) [] []
Right (Lam "x" (Vari "x"))
```

- This is polymorphic id; it won't typecheck, though. As with any type system, we exclude some programs we know to be valid ("valid" not being precisely defined - it may not even be self-consistent.)

````
substCheckEvalAnn (Lam "x" (Vari "x")) [] []
Left "...your term can't have a type inferred for it..."
````

- This is polymorphic id. We need two arguments - one for the type; for the value itself; we need to bind these two variables *twice* - once in the term; once in the type. This ∀a:* is *not* the same semantic mechanism as a Hindley-Milner ∀a:*. The first knows the value of `a` when it is bound by the *evaluator*; the second by a *unifier*. Some of the larger-scale implementations of dependent types allow us to elide the type arguments by declaring them as implicit.

```
Idris> substCheckEvalAnn
  (Ann (Lam "a"
          (Lam "x" (Vari "x")))
       (Pi "a" Star
          (Pi "x" (Vari "a") (Vari "a"))))
  [] []
Right (Lam "a" (Lam "x" (Vari "x")))
```

And now, with the help of our REPL language interpreter, we can explore applications.

- This is the same polymorphic id, first partially applied to the type Star: we get standard id in return.

```
Idris> replEval [
  Define "id" (Lam "a"
                (Lam "x" (Vari "x")))
              (Pi "a" Star
                (Pi "x" (Vari "a") (Vari "a"))),
  Define "idStar" (App (Vari "id") Star) (Pi "x" Star Star)
]
Right (Lam "x" (Vari "x"))
```

- Now apply the partially-applied id once more to Star.

```
idris> replEval [
  Define "id" (Lam "a"
                (Lam "x" (Vari "x")))
              (Pi "a" Star
                (Pi "x" (Vari "a") (Vari "a"))),
  Define "idStar" (App (Vari "id") Star) (Pi "x" Star Star),
  Lift (App (Vari "idStar") Star)]
Right (Ann Star Star)
```

Last notes
----------

We come to the same conclusion as Löh et al.: the the ability to express dependent types isn't terribly useful without the ability to express any form of tye types with constructors that give these types their inhabitants, and ways of deconstructing the inhabitants of these types - their eliminators. If we want our languages to be concise, does this necessarily mean new syntactic forms for inductive families and pattern matching? Another core language ΠΣ, as described in "ΠΣ: Dependent Types without the Sugar" by Altenkirch et al.- tries to get more mileage out of the humble `=`, although we won't try a description here.

A teaser, though: finite sets in the style of Fin have a `case` form as their eliminator; dependent products of the form `(x:τ, y(x))` have a `split` form as their eliminator. But their use isn't fully declarative: a boxing notation `[x]` is used to ensure that `x` is only expanded in the form `![x]`; this ensures that the evaluation of bodies in λ literals terminates. In their terms: "type checking a dependently typed program can involve evaluation under binders." Note the "can": Agda, as we have noted earlier, does not do this.

Other notes.

- Remember what makes statically evaluating types dependent on runtime values possible: the fact that "eval", in the absence of information, can return partially-evaluated terms when it needs to. (This does not include evaluation "under" λ abstractions!) Here's an example in Idris, for example: remove `infer`'s case for Pi, and
`(substCheckEvalAnn (Pi "x" Star Star) [] [])`, fails at runtime:
```
*** Micro.lidr:247:1:unmatched case in Micro.infer ***
```
The typechecker, though, left the term partially evaluated, simultaneously inlining it into its call site - a use of `>>=`:
```
(Prelude.Either e implementation of Prelude.Monad.Monad, method >>= String) (infer (Pi "x" Star Star) []) (\ty' => ...and so on and so forth.
```

- The vast majority of dependently-typed languages have implicit arguments in Pi types whose values can be inferred by unification - something similiar to `a` in
```
  cons : {a : Type} -> a -> List a -> List a
````
A hand-unifier would make the following deductions in the case of Cons 4 [1, 2, 3]:
```
  List a = List Nat
  a = Nat
```
Is this desugared to explicit application on Nat? This would require destructuring the List Nat term - and this destructuring is not defined within λ_Π. This is still a non-trivial feature, and one that seems ad-hoc.

That's it. Go extend, reformulate, clarify.