Twelf style guide

From The Twelf Project
Jump to: navigation, search

This page is a style guide for Twelf code. For a style guide for contributions to the Twelf Project Wiki, see Project:Style guide

The style you use to write Twelf code should be consistent so that it is readable by others now and by you in the future. However, the general objectives of consistency and readability of code is more important than anything that is or possibly could be said on this page. Therefore, this page should be seen as attempt to collect a set of good practices from experience that can be used as recommendations for new users.

The first two sections are about whitespace & comments, which are extremely important aspects of readability. The final section is on conventions used for writing identifiers, which is less important as long as consistency is maintained within a project. The article on naming conventions also considers ways of standardizing identifier names.

Whitespace

Proper use of whitespace, line breaks, and spacing is very important for promoting the readability of Twelf code.

Object language syntax

The declarations for the constants corresponding to a type for syntax of an object language should be grouped together. There should be an empty line between the declaration of the type and its constants. There should be a line break, but no empty lines, between each declaration.

color : type.

color/red   : color.
color/black : color.

Judgments

The declarations for the constants corresponding to the inference rules for a particular judgment should be grouped together. There should be an empty line between the declaration of the judgment and its inference rules, as well as one empty line between the declaration of two inference rules. If a %mode declaration is used, it should be on the line immediately following the declaration of the judgment.

color-neq : color -> color -> type.

color-neq/red-black : color-neq color/red color/black.

color-neq/black-red : color-neq color/black color/red.



color-swap : color -> color -> type.
%mode color-swap +C1 -C2.

color-swap/red : color-swap color/red color/black.

color-swap/black : color-swap color/black color/red.

Metatheorems

The definitions for cases to a metatheorem should be grouped together. The %mode declaration should be on the line following the declaration of the type family for the metatheorem, with no line breaks in between. There should be an empty line following the mode declaration. There should be one empty line between each case. There should be an empty line preceding the %worlds declaration. The %total declaration should be on the following line.

can-color-neq : {C:color} color-neq C C' -> type.
%mode color-neq +D1 -D2.

- : can-color-neq color/red color-neq/red-black.

- : can-color-neq color/black color-neq/black-red.

%worlds () (color-neq _ _).
%total {} (color-neq _ _).

Additional guidelines

  • There should be at least 3 empty lines between any "groups", where a group is something on the scale of declarations for a type family or proof of a metatheorem. 4 or more empty lines should between super-groups of related groups, such as the proofs for a set of related lemmas.
  • The colons following the names of the constants for a group should all line up.
  • Directives such as %mode, %reduces, %terminates, %worlds, %total should be at the start of a new line. The one exception to this rule is the fixity directives such as %infix - it is often clearest to put the fixity declaration for a constructor on the same line as the declaration of that constructor.

Comments

Comments are at least as important a consideration when writing Twelf code intended to be readable by others, especially when the other readers are not themselves Twelf users. The CMU POPLMark solution contains a good representation of how comments can be used to aid comprehension of a proof.

Guidelines

  • Each file should begin with single-line comments establishing a title and authorship. If several more lines about the purpose of the file are needed, those should go into a multi-line comment immediately underneath the title/author information.
  • Single line comments should annotate most "groups" and "super-groups" explaining, briefly, their purpose. They should be associated with a relatively strong visual indicator that is consistent across the file, such as one of the following. Be conscious of the interaction of your comment style with the Twelf Emacs mode syntax highlighting – some comment styles which use percent signs at the end and the beginning of a line cause the syntax highlighting to behave unpredictably.
%%%%% Syntax %%%%%
% ===== Type system ===== 
%%----- Theorems about termination behavior -----
% ******* The result is s(s(s nat-39)) ******* 
%%%%% Metatheorems about nat
%%%%{ Type preservation }%%%%
  • Comments are most useful as multi-line comments at the beginning of "groups" and "super-groups" as defined in the previous section. Listing the important metatheorems at the beginning of a long group of metatheorems is also helpful.
  • Multi-line comments should be as free of visual cruft (borders, horizontal lines) as possible. The %{ }% construct should be used for most multi-line comments.

Identifiers

Due to the current absence of a module system for Twelf, careful identifier choice is crucial to managing the namespace of a large project. Because small projects can often grow into something quite large, we suggest thinking about a system of conventions such as the one described here from the outset.

The names of constants and type families should always begin with a lower case letter. Type families should only contain lower-case letters, numbers, and dashes ("-") which are used to separate words in an identifier, as in this-is-my-neat-proof. The other options using underscores (as in this_is_my_neat_proof), an option that is often used but which is currently generally avoided. Using camelCase is generally to be avoided: it is easier to distinguish an implicit parameter from a constant if only implicit parameters use capital letters.

Implicit parameters must be capitalized; when using explicit parametersit is sometimes clearer to capitalize them, but it is often more clear and less error-prone to make explicit parameters lower case.

Twelf code can generally be sorted into one of three categories: object logic syntax, judgments about the object logic syntax and other judgments, and metatheorems about the object logic. Each of the three categories has distinct style conventions.

In this section, conventions will only be given as to how to structure identifiers with separators such as "-" and "/" to make then more readable and organized. There is a separate guide for naming conventions which suggests what words should go between such separators.

The natural numbers will be used as a running example.

Object language syntax

nat : type. 
list-nat : type.

Type families are typically inhabited by constants that correspond to different pieces of syntax or inference rules. We use a slash ("/") between the name of the type family and the identifier for the individual rule.

nat/z : nat.
nat/s : nat -> nat.

list-nat/nil : list-nat.
list-nat/cons : nat -> list-nat -> list-nat.

(Whether a list of natural numbers should be called list-nat or nat-list is a matter left to the naming conventions article.)

Abbreviations

The disadvantage of this representation is that identifier names can get relatively long.

There are two solutions for this. One is that, if you are defining a language or logic, and not a library to be used in another project, you may want to consider a small number of pieces of syntax your "leaf cases" and simply leave off the part before the forward slash. Be careful if you are doing so; this will seem like a great idea until you realize that you need both an element of type and an element of syntax called cont or pair or tuple.

The other solution is to use an abbreviation or a notational definition.

% Example of abbreviation

%abbrev z = nat/z.
%abbrev s = nat/s.

% Example of notational definition

z = nat/z.
s = nat/s.

Abbreviations are probably better for large projects, because even if the abbreviated identifier gets redefined, it appears in the unshadowed extended form in the Twelf buffer. Notational definitions are probably preferable for small projects - or projects which are being debugged - for the same reason: shorter, more informative identifiers will appear in the Twelf buffer.

Judgments

The naming conventions for judgments and their inference rules are similar to the ones for object syntax. The part after the forward slash, if it is associated with a piece of relevant syntax (i.e. /cons or /s) should use the same modifier.

plus-nat : nat -> nat -> nat -> type.
%mode plus-nat +N1 +N2 -N3.

plus-nat/z : plus-nat z N N.

plus-nat/s : plus-nat (s N1) N2 (s N3)
               <- plus-nat N1 N2 N3.

Metatheorems

Identifier names

Each metatheorem is given a name in Twelf. There are two ways in which someone might consider naming their metatheorems. If you are defining a metatheorem that defines an admissible rule, it may be reasonable to use the convention used for showing inference rules:

plus-nat/z-alt : {N} plus-nat N z N -> type.
%mode plus-nat/z-alt +N -D.

In most other cases, however, it is more reasonable to simply name the lemma using words and hyphens:

plus-comm : plus-nat N1 N2 N3 -> plus-nat N2 N1 N3 -> type.
%mode plus-comm +D1 -D2.

Case names

The cases in a metatheoretic proof almost never need to be referred to, so it is common to name the labels for every individual case -. This may, however, make it more difficult to correlate error messages with specific rules, and so should be done with care.

plus-nat/z-alt : {N} plus-nat N z N -> type.
%mode plus-nat/z-alt +N -D.

- : plus-nat/z-alt z plus-nat/z.

- : plus-nat/z-alt (s N) (plus-nat/s D) 
      <- plus-nat/z-alt N D.

%worlds () (plus-nat/z-alt _ _).
%total T (plus-nat/z-alt T _).

If it is preferable to give each case of a metatheorem a name, for debugging or clarity reasons, the convention is to put a - before an identifier for the case. For example, we could re-write the preceding theorem in the following way.

plus-nat/z-alt : {N} plus-nat N z N -> type.
%mode plus-nat/z-alt +N -D.

-z : plus-nat/z-alt z plus-nat/z.

-s : plus-nat/z-alt (s N) (plus-nat/s D) 
      <- plus-nat/z-alt N D.

%worlds () (plus-nat/z-alt _ _).
%total T (plus-nat/z-alt T _).

Example signature

%% Demonstration of good Twelf style
%% The Twelf Wiki authors, Febtober 19045

%{

If we needed to say a bit more about what we were doing
here than just the line or two that fits at the top of the
page, then this would be about the right place to try
and put that in.

}%



%%%%%{ Syntax }%%%%%

exp : type.

exp/unit : exp.



%%%%%{ Types }%%%%%

tp : type.

tp/unit : tp.




%%%%%{ Judgments }%%%%%

typed : exp -> tp -> type.
%mode typed +E -T.

typed/unit : typed exp/unit tp/unit.



isvalue : exp -> type.
%mode isvalue +E.

isvalue/unit : isvalue exp/unit.




%%%%%{ Metatheorems }%%%%%

%{

We're only proving one, rather silly, methatheorem in this style example,
namely that if an expression is a value then it has a type. Of course,
we're relying on the fact that everything in our toy language is a value
and has a type.

}%

isvalue-implies-typed : isvalue E -> typed E T -> type.
%mode isvalue-implies-typed +D1 -D2.

- : isvalue-implies-typed isvalue/unit typed/unit.

%worlds () (isvalue-implies-typed _ _).
%total T (isvalue-implies-typed T _).