Expressions

In the directory tests you can find some files that provide example declarations for the different modes. They might offer a quick overview about the syntax of s, f, fw, cc, r, rg, un. The following will give you an overview of the syntax starting with S. For all the other calculi only the extensions are explained.

S - Simply Typed $\lambda$-Calculus

The following constructs are available in the simply typed mode:

Expression	Syntax	Note
$\lambda x:E_1.E_2$	\x:E1.E2	abstraction
$\Pi X:E_1.E_2$	pi X:E1.E2	quantification
$E_1\rightarrow E_2$	E1->E2	type, abbreviation for $\Pi _:E_1.E_2$
$\mu X.E$	mu X.E	built-in iso-recursive types
	E1 E2	application
	fold E1 E2	folds the iso-recursive type of E2 once according to E1
	unfold E1 E2	unfolds the iso-recursive type E1 of E2 once
	x	identifier $(a\dots z\vert A\dots Z\vert ')(\_\vert a\dots z\vert A\dots Z\vert 0\dots 9\vert ')^{\ast}$
	~12+3**(5-4)	built-in integers and all available arithmetic operations on them
	3=3	comparison on integers,
		further operators are <<,<=, >>, >=, <> (unequal)
	true and false	boolean values
	not E	negation of boolean values
	unit	unit value
	Int, Bool, Unit	built-in base types
	if E1 then E2 else E3	conditional
	E1 as E2	ascription; both expressions must be atomic
	{x=E1,y=E2}	records
	record@field	record projection
	{x:E1,y:E2}	record types
	<x=E1> as E2	variant
	<x:E1,y:e2>	variant types
	case E of <l1=x1> => E1 | ... | <ln=xn> => En	case construct to access a value inside a variant; due to the uniform syntax you have to put parentheses around E$_1$,...,E$_n$ except for atomic and arithmetic expressions.
	ref E	creates a reference for E
	!E	dereferences E
	E1 := E2	assignment
	let x=E1 in E2	let expression, but only terms can be bound

Be aware of the operator for multiplication **, the smaller test << and the greater test >> that are somewhat unconventional. In S,F and Fw records and variants can only contain terms. Moreover a label cannot be used more than once in the same expression.
An expression sequence (E1;...;En) is available as syntactic sugar. The sequence (E1;E2) is transformed into an application (\x:Unit.E2) E1. Therefore type errors in a sequence might be a bit inconvenient. A expression sequence is useful when you are working with references.

F - System F

In addition to S terms may depend on types and you have universally quantified types. This is expressed in the following way:

Expression	Syntax	Note
$\lambda X.E$	\X.E	type abstraction
$\forall X.E$	\/X.E	the type of a type abstraction
		(abbreviation for $\Pi X:E_1.E_2$)

Fw - F$\omega$

Type operators are available, i.e. types may be abstracted out of types. Additionally the notion of kinds is introduced. Kinds are the types of types.

Expression	Syntax	Note
$\star$	*	base kind $\star$
$\lambda x:E_1.E_2$	\x:E1.E2	$E_1$ might be a kind like $\star\rightarrow\star$
$\forall X:E_1.E_2$	\/X:E1.E2	$E_1$ might be a kind like $\star\rightarrow\star$

CC - Calculus of Construction

This is the richest available calculus. Now you can abstract terms out of types. The syntax does not change. if and case can be used on type level, i.e. you can write things like if E then Int else Bool. Records and variants can contain both terms and types at the same time. There is a syntactic sugared version of $\Pi x:Int.T$, namely $(x::Int)\rightarrow T$.

R - Type Reconstruction for Prenex Polymorphism

Expression	Syntax	Note
$\lambda x.E$	\x.E2	blank lambda abstraction
$\lambda f:\alpha\rightarrow\beta$.E	\f:'a->'b.E	use of free type variables

Do not confuse the blank lambda abstraction with the abbreviation in F, Fw and CC or the abstraction in untyped mode. There is the possibility to annotate a term with free type variables and all types from S mode. Therefore the expression \x.E can be seen as an abbreviation for \x:'a.E where 'a is not used in the enclosing context.
This mode does not offer the full functionality of the previous ones. It consists of the basic elements which are lambda abstraction, application and variables. Additionally all basic types, terms and operations are integrated, i.e. numbers, boolean, unit, +,-, if-expression, ... . Records are also available. However be aware that these are different from the other constructs in an important way: the constraint typing algorithm may fail if there is a wrong projection.
As a challenge you can try to implement further constructs. Variants are for example very similar to records.

RG - Type Reconstruction Based on Graphs

In RG there are equi-recursive types. So you do not have to annotate terms with self application with a fold or unfold expression, i.e. the expression $\lambda x. x\:x$ is type correct and gets the type:

- \x. x x;
> def it = <fun> : (mu A.A->'a)->'a

In the other respects the mode is just the same as R (but records are not available).
Iso-recursive types, let expressions, records, variants and references are not integrated into this mode.

U - Untyped Lambda Cube

In this mode the type checker is switched off. Type annotations are ignored. So it is permitted to input senseless expressions without any kind of error message. But of course this will often lead to stuck terms which cannot evaluated further.

UD - User Defined

In this mode the type checker and evaluator are set to the user's implementation. The user may implement the functions in UserCheckEval.sml. You can find explanation and an example implementation in this file in the directory src of the Cubint package.

SUB - Subtyping

This mode provides subtyping for variants and records and can be enabled in the typing modes s,f,fw and cc. There is no Top type integrated in the calculus. Therefore the interpreter does not accept input like if true then 3 else true as a value of type Top is not very valuable. In subtyping mode you can leave out the variant ascription.