# Contextual LF¶

In contrast with languages such as Coq or Agda that feature full dependent types, Beluga has an indexed type system. This is a restricted form of dependent types in which one quantifies only over a specific index domain. The index domain of Beluga is Contextual LF.

At a high level, a Contextual LF object (or type) is an LF term (or type) together with an LF context in which the term (or type) makes sense. For example, consider the following syntax of types for the simply-typed lambda calculus together with a structural equality relation on types.

```LF tp : type =
| base : tp
| arr : tp -> tp -> tp
;

LF eq : tp -> tp -> type =
| eq_base : eq base base
| eq_arr : eq A1 A2 -> eq B1 B2 ->
% ------------------------
eq (arr A1 B1) (arr A2 B2)
;
```

The contextual object that encodes a closed proof that the `base` type is equal to the `base` type is `|- eq_base`. We write this sometimes with parentheses to make reading easier, e.g. `( |- eq_base )`.

Open terms can be represented by using a nonempty LF context. For example,

```x : eq A B |- eq_arr x eq_base
```

is a contextual object of type `x : eq A B |- eq (arr A base) (arr B base)`.

## Computation types¶

Contextual LF objects and types may be boxed into computation types. These types are primarily used for encoding theorems about a formal system. For example, the type of a theorem expressing that equality is reflexive would be

```{A : |- tp} [ |- eq A A]
```

We read this as “for all (closed) types `A` , `A` is equal to itself.” This is a computation type. It is composed of two parts in this example: a PiBox-type and a box-type. The PiBox is used as a quantifier; we will go into more depth on this in the following section. The syntax `[ |- eq A A ]` is a boxed contextual type: any contextual type may be surrounded by a box `[ ]` to embed it as a base computation type. Similarly, contextual objects may be boxed to form computation expressions.

Another example theorem `trans`, that equality is transitive, can be expressed as

```[ |- eq A B] -> [ |- eq B C] -> [ |- eq A C]
```

Similar to in a pure LF type (see here), free metavariables appearing in a computation type are automatically abstracted over using PiBox at the front. So really, the above example type is elaborated into

```{A : |- tp} {B : |- tp} {C : |- tp}
[ |- eq A B] -> [ |- eq B C] -> [ |- eq A C]
```

But again as in a pure LF type, these quantifiers are implicit and there is no way for a programmer to explicitly supply an instantiation for them. The instantiations are found when the theorem `trans` is used.

This example illustrates the simple function space, written with the arrow `->`. In Beluga, the dependent function space (using the PiBox syntax) is separate from the simple function space (using the arrow syntax).

To recap, the formal grammar of computation types is the following.

where `B` denotes an inductive type and `U` denotes a contextual type. The remaining two forms are the simple and dependent function space, respectively.

## Metavariables¶

The syntax `{A : |- tp} ...` expresses what’s called a PiBox-type. This example quantifies over the contextual type `|- tp` and binds `A` as a metavariable. Whenever a metavariable is used, as `A` is used for example in `eq A A`, it is given a substitution. This substitution mediates between the LF context of the metavariable and the LF context at the use site. If no explicit substitution is provided, an identity substitution is assumed. An identity substitution is sufficient in the example because the context of both the metavariable and its use site is the empty context.

For example, suppose we have the metavariable ```X : (x : tm, y : tm |- tp)```. (Perhaps `X` refers to `x, y |- arr x y`.) Then, ```X[base, base] : |- tp```. Here we use an explicit substitution to instantiate the bound variables `x` and `y`.

## Context variables and schemas¶

Beluga provides a mechanism for abstracting over and quantifying over contexts. An abstract context is referred to by a context variable. A context variable is a special form of metavariable.

Whereas kinds classify types, contexts are classified by schemas. A schema essentially lists the possible types of the variables occurring in the context. The following declaration defines a schema `ctx` that can contain only types.

```schema ctx = tp;
```

Before we can elaborate an example demonstrating context variables, first consider the following syntax of terms for the simply typed lambda calculus as well as a typing judgment for this language.

```LF tm : type =
| app : tm -> tm -> tm
| lam : tp -> (tm -> tm) -> tm
;

LF oft : tm -> tp -> type =
| t_app : oft M (arr A B) -> oft N A ->
% ---------------------------
oft (app M N) B

| t_lam : ({x : tm} oft x A -> oft (M x) B) ->
% ----------------------------------
oft (lam A M) (arr A B)
```

This syntax of terms includes a type annotation on lambda abstractions, and the typing judgment ensures that it is the type given in the annotation that is used as the parameter `x`’s type in the premise of the `t_lam` rule.

This language admits type uniqueness. That is, given two typing derivations for the same term, the types assigned to that term must be equal. We can state this theorem as a computation type in Beluga as follows.

```(g : ctx) [g |- oft M A1[]] -> [g |- oft M A2[]] -> [|- eq A1 A2]
```

First, notice the syntax `(g : ctx) ...`. This is called implicit context quantification. Unlike for ordinary implicit metavariables such as `M`, the schema of an implicit context variable cannot be inferred by type reconstruction. Therefore, one must use implicit context quantification to explicitly specify the schema of the context variable.

Second, notice that the metavariables `A1` and `A2`, referring to types, are associated with the substitution `[]` in the assumptions of the theorem. Type reconstruction is in some sense a greedy algorithm, so had these substitutions been left out, the type of `A1`, upon appearing in `g |- oft M A1`, would be `g |- tp`. But this makes no sense because types ought to be closed in the simply-typed lambda calculus. To specify that the metavariables `A1` and `A2` must be closed, we associate them with a weakening substitution `[]`. This way, type reconstruction will correct infer that the context of these metavariables is empty.

Confusingly, the reported error had the weakening substitutions been omitted would be relating to the occurrences of `A1` and `A2` in ```|- eq A1 A2```. Here, the implicit identity substitution would be ill-typed. Recall that the type of `A1`, for instance, would have been inferred as `g |- tp` and the identity subsitution would need to send the metavariable’s context `g` to the empty context, which it does not. In general, when dealing with ill-typed substitution errors, it is worth paying close attention to every occurrence of any relevant metavariables.

## Unboxing¶

When one has a computational variable referring of a boxed contextual type, one frequently likes to promote this variable to a metavariable. This process is called unboxing. For example, suppose we have the assumption `x : [|- tp]`.

• In Beluga, one writes `let [_ |- X] = x in ...` in order to unbox `x` as the metavariable `X`.
• In Harpoon, one uses the `unbox` tactic for this: `unbox x as X`.