An _algebraic signature_ describes the structure of a set of terms.
A signature introduces one or more _AlgebraicSorts_, i.e., collections of terms.
Sorts are inhabited by declaring _TermConstructors_. A constructor has a name and
zero or more subterms. A constructor is declared by stating its name, the list of
sorts of its direc subterms and the sort of the constructed term.
Constructor names may be overloaded.
The sorts =String= and =Int= are predefined.
A typical example of a signature is the following description of LambdaCalculus expressions.
signature
sorts Exp
constructors
Var : String -> Exp
App : Exp * Exp -> Exp
Abs : String * Exp -> Exp
---+++ Term Injections
A term injection is a constructor-less constructor in a signature.
Example:
signature
sorts Var Exp
constructors
Var : String -> Var
: Var -> Exp
Abs : Var * Exp -> Exp
Issues
* FixedLengthTuple
* TermAnnotation
* PolymorphicTypes
-- Main.EelcoVisser - 09 Dec 2001

-----
CategoryGlossary