Syntax of LLF
Concrete syntax
The LLF terms rendered on the leftmost column are written using the concrete
syntax on the right. Dependent terms and the linear arrow can be written in
different forms.
| Kinds |
| type |
type |
| Pi x:A.K |
{x:A}K |
A -> K |
K <- A |
|
| Types |
| P M |
P M |
| T (top) |
<T> |
| A & B |
A & B |
| A -o B |
A -o B |
B o- A |
| Pi x:A.B |
{x:A}B |
A -> B |
B <- A |
|
| Objects |
| <> |
() |
| <M, N> |
(M, N) |
| fst M |
<fst> M |
| snd M |
<snd> M |
| lambda^ x:A. M |
[x^A]M |
| M ^ N |
M ^ N |
| lambda x:A. M |
[x:A]M |
| M N |
M N |
Precedence of the operators
The following table indicates the precedence and the associativity of the
LLF operators in the concrete syntax. Use parenthesis for grouping.
| highest |
<fst> <snd> |
prefix |
|
(juxtaposition) ^ |
left associative |
|
& |
right associative |
|
-> -o |
right associative |
|
<- o- |
left associative |
|
{} [] [^] |
prefix |
| lowest |
, |
right associative |
Conventions
The verbosity of an LLF signature can be cut by more than half in average
by adopting simple conventions and by relying on automatic methods to
reconstruct information kept implicit. This has major benefits in terms
of readability of an LLF program, and in terms of usability of the language.
- The type of the variables introduced in Pi's and lambda's are kept
implicit whenever possible. Although the problem of recovering these
types is in general undecidable, very few programs require them to be
explicit in practice.
The syntax
[x], [x^] and
{x} is the implicit form of [x:A],
[x^A] and {x:A}, respectively.
- Dependent types enclosing completely a declaration in the signature
can be omitted altogether. The introduced variables should however
begin with an uppercase letter.
- Dependent types
{x:A}B such that the variable
x does not occur in B can
be written A -> B or B <- A.
Similarly for kinds.
- Juxtaposition is used also for linear application (i.e. we write
M N for M^N). Again, it might
not be possible to decide whether an application is linear or
intuitionistic, but in most case it is. In case of ambiguity,
it is enough to provide additional typing information.
Last modified: 14 December 1995
Iliano Cervesato
()
and
Frank Pfenning
()