Implicit and explicit parameters

When declaring a type family or constant, the STELF 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. STELF 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, STELF 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 STELF output is included - note that the STELF 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 STELF.

Implicit parameters

(options removed from twelftag: hidden=true)

%sort exp %.
%sort typ %.
%sort of {_ exp} {_ typ} %.
%term 0 exp %.
%term 1 exp %.
%term bit typ %.
%term void typ %.
%term of1 of 1 bit %.
%term of0 of 0 bit %.

(options removed from twelftag: discard=true check=decl)

%sort translate-i {_ of M A} {_ of M' A} %.
%mode translate-i %in %out %.

Explicit parameters

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

(options removed from twelftag: discard=true check=decl)

%sort translate-e {M exp} {A typ} {M' exp} {_ of M A} {_ of M' A} %.
%mode translate-e %in %in %out %in %out %.

See also

• Full LF discusses implicit and explicit parameters in the section “STELF conveniences.”