Implicit and explicit parameters

From The Twelf Project
(Redirected from Explicit parameter)
Jump to: navigation, search

When declaring a type family or constant, the Twelf programmer often needs to use universally quantified parameters, and has the choice of making the parameter implicit or explicit. The article on converting between implicit and explicit parameters discusses how these two ways of doing things can be derived from each other.

Using fully explicit parameters means that all variables are bound by being placed within curly braces {}. The type family or constant generally has more arguments when using this form.

Using implicit parameters means that variables are not put within curly braces. Twelf assumes an identifier is meant to be a universally quantified parameter if the identifier starts with an uppercase letter and if that identifier has not been bound or defined anywhere else. This is essentially an interface aspect allowing for simpler code—internally, Twelf applies type reconstruction to identify the type of the universally quantified variables and converts the implicit parameters into explicit parameters.

The implicit parameters style is more concise and is often cleaner; however, in some cases it is necessary to use explicit parameters (for instance, a %terminates or %total declaration can refer to explicit parameters, not implicit parameters), and it may make stylistic sense in other situations as well.

Examples of the two different styles follow, using the language from the article on converting between implicit and explicit parameters which is omitted for brevity. The Twelf output is included - note that the Twelf output always writes out explicit parameters,[?] even if the definition is using implicit parameters; therefore the two examples have almost exactly the same output from Twelf.

Implicit parameters

translate-i : of M A -> of M' A -> type.
%mode translate-i +D -D'.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

translate-i : {M:exp} {A:typ} {M':exp} of M A -> of M' A -> type. %mode +{M:exp} +{A:typ} -{M':exp} +{D:of M A} -{D':of M' A} (translate-i D D').

%% OK %%

Explicit parameters

Note that in this example we use slightly bad style, capitalizing our bound variables M, A, and M'.

translate-e : {M : exp}{A : typ} {M' : exp} of M A -> of M' A -> type.
%mode translate-e +M +A -M' +D -D'.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

translate-e : {M:exp} {A:typ} {M':exp} of M A -> of M' A -> type. %mode +{M:exp} +{A:typ} -{M':exp} +{D:of M A} -{D':of M' A} (translate-e M A M' D D').

%% OK %%

See also