General Recursion in Type Theory :

A non-trivial example: Unification

Part 1: data types

type Var = Int type Fun = Int data Term = Var Var | Fun Fun [Term] type Assignment = (Var,Term) type Substitution = [Assignment] type Equation = (Term,Term) type Equations = [Equation]