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 unboxx
as the metavariableX
. - In Harpoon, one uses the
unbox
tactic for this:unbox x as X
.