Coding Conventions

Text File Syntax Issues: Tabs and Spaces

ML files typically have many levels of indentation, so please set the indent width to be 2 characters. Do not use tab characters.

In emacs, you can do this by having the following in .emacs file:

(custom-set-variables
 '(tab-width 2) ;; tab width of 2 please
 '(indent-tabs-mode nil) ;; no tabs
)

ML Coding Style

Provide Pretty Printing Code

To help make debugging feasible: every type, T should have a pretty : T -> Pretty.T function. It can be handy to have a print one too: val print = Pretty.writeln o pretty. The Isabelle file src/Pure/Generic/pretty.ML is the pretty printing library I use.

Structure Your Code

Try to put types into structures that manipulate and work with them. Put these structures into their own file is they get big (over a few pages of code).

Pairing and Records

Pairing should be used when you think that those items of data will stay together (be passed by sub-functions together) or belong together in some way. Otherwise use currying as it is more flexible.

Records are a nice way than pairing for storing lots of things.

Records should have get, set and update functions for low level manipulation/inspection. I write these like this:

datatype foo = Foo of { field1 : ty1, ..., fieldn : tyn }

fun get_field1 (Foo rep) = #field1 rep;
fun update_field1 f (Foo rep) = Foo { field1 = f(#field1 rep), ... fieldn = #fieldn rep };
val set_field1  = update_field1 o K;
...

Curried Argument Order

When working with functions that modify data, let the given data item to be modified be the last argument. When examining data in different ways, let the data item be the first argument. This way you easily fold over modifications and curry getting information etc.

For example, given a datatype of tables 'a Table, the update function should look like:

update : key * 'a -> 'a table -> 'a table

and the get element should look like:

get : 'a table -> key -> 'a