Judgements

In Typol, sequents are rigorously typed and must be declared at the beginning of a program by a judgement declaration. The judgement declares a syntactic form that may be used throughout the program. The form consists of expressions and symbols. The expressions may be any of the following:

• The name of a phylum from one of the formalisms used at by the program. All formalisms used in a program must be declared in a use clause at the beginning of the program.
• A formalism name, which stands for all of its phyla.
• The predefined Typol types integer, string, and path.
• The anonymous variable underscore (_), which corresponds to any type.

For example, the judgement:

EXP : INTEGER

declares that expression to the left of the colon must be an abstract syntax tree pattern whose associated operator belongs to the phylum EXP. To the right of the colon, the pattern's associated operator must belong to the phylum INTEGER.

The profile of the judgement -the number and syntax of symbols and the number of elements in the hypotheses and consequents- may only appear once in a program. For example, the following judgements could not both appear in the same program:

   judgement ENV |- DECLS -> ENV
   judgement ENV |- RULES -> ENV

A sequent that doesn't respect the abstract syntax constraints imposed by the judgement is rejected by the Typol type checker.

What judgement(s) should we declare for The most natural response is:

judgement EXP : INTEGER

However, we want to evaluate not only an expression, but a list of expressions (phylum EXP_S). We can either add a second judgement to handle an expression list, create a larger phylum to englobe both EXP and EXP_S, or use the language name to allow all Exp phlya. We choose the later solution for the sake of simplicity, but we discourage this choice in general because it allows overly permissive, weakly typed semantic rules.

To the right of the colon, we specify INTEGER, which contains the operator integer, the lone operator in Exp that expresses a value. Our judgement declaration therefore has the form:

judgement Exp : INTEGER