Converting between implicit and explicit parameters

From The Twelf Project

When declaring a type family or constant, the Twelf programmer often has a choice between implicit and explicit parameters for some arguments. There is no reason to fret over this choice, for there is an easy technique for converting between implicit and explicit parameters.

Suppose we have a language defined as follows:

exp : type.
typ : type.
of  : exp -> typ -> type.

0 : exp.
1 : exp.
bit : typ.
void : typ.
of1 : of 1 bit.
of0 : of 0 bit.

We wish to define a translation between type derivations in this language, as a part of a source to source translation. The implicit and explicit versions are as follows:

ERROR: option 'noinclude' deprecated or invalid

% implicit version
translate-i : of M A -> of M' A -> type.
%mode translate-i +D -D'.

% explicit version
translate-e : {m : exp}{a : typ} {m' : exp}
              of m a -> of m' a -> type.
%mode translate-e +M +A -M' +D -D'.

[edit] Defining explicit in terms of implicit

Suppose we choose the implicit version and implement it, but later decide we prefer the explicit version. We can then define the explicit version in terms of the implicit one by simply leaving out arguments:

 implicit version
translate-i : of M A -> of M' A -> type.
%mode translate-i +D -D'.

translate-i1 : translate-i of1 of0.
translate-i0 : translate-i of0 of1.


 explicit version
translate-e : {m : exp}{a : typ} {m' : exp}
              of m a -> of m' a -> type.
%mode translate-e +M +A -M' +D -D'.

translate-e/i : translate-e M A M' D D' <- translate-i D D'.

%worlds () (translate-i _ _) (translate-e _ _ _ _ _).
%total D (translate-i D _).

%total D (translate-e _ _ _ D _).

[edit] Defining implicit in terms of explicit

Suppose we define the explicit version, and then choose to define the implicit version in terms of the explicit:

 explicit version
translate2-e : {m : exp}{a : typ} {m' : exp}
               of m a -> of m' a -> type.
%mode translate2-e +M +A -M' +D -D'.

translate2-e1 : translate2-e 1 bit 0 of1 of0.
translate2-e1 : translate2-e 0 bit 1 of0 of1.

 implicit version
translate2-i : of M A -> of M' A -> type.
%mode translate2-i +D -D'.

translate2-i/e : translate2-i D D' <- translate2-e _ _ _ D D'.

%worlds () (translate2-i _ _) (translate2-e _ _ _ _ _).

%total D (translate2-e _ _ _ D _).
%total D (translate2-i D _).

Twelf is able to deduce via its term reconstruction algorithm what M, M' and A are, so this is well-moded.

[edit] Using annotations

Sometimes Twelf's term reconstruction algorithm is not powerful enough to automatically recover explicit parameters from implicit ones.^[?] In general, one may use type annotations to get access to the implicit parameters to a relation. For example, we may write the translate2-i/e constant above as:

ERROR: option 'noinclude' deprecated or invalid

translate2-i/e : translate2-i (D : of M A) D' <- translate2-e M A M' D D'.

Here we have access to the implicit inputs M and A, gleaned from the dependent type of D.

All code for this tutorial. Twelf's output for this tutorial.

---

This is a tutorial that has been identified as needing to be extended, expanded, and or improved, and which does not yet a contain a full explanation of what it is meant to address. We're getting to it, leave a message for us on the discussion page or elsewhere if you need this information and we'll probably get to it faster.