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