Documentation

Pretty instance for type signatures.

Two type signatures are similar if they annotate the type of the same functions with similar types.

 Γ ⊢ τ ≈ τ'
————————————————————————————————————————
 Γ ⊢ f₁, … , fₙ :: τ ≈ f₁, … , fₙ :: τ'

Pretty instance for function declarations.

Instance to get the name of a function declaration.

Strips the expression type annotations from function declarations.

Two function declarations are similar if their right-hand sides are similar under an extended Renaming that maps the corresponding type arguments and arguments to each other. If the arguments are annotated, their type annotations must be similar under an extended Renaming that maps the corresponding type arguments to each other.

 Γ ∪ { α₁ ↦ β₁, …, αₘ ↦ βₘ, x₁ ↦ y₁, …, xₙ ↦ yₙ } ⊢ e ≈ f
 Γ ∪ { α₁ ↦ β₁, …, αₘ ↦ βₘ } ⊢ p₁ ≈ q₁, …,
 Γ ∪ { α₁ ↦ β₁, …, αₘ ↦ βₘ } ⊢ pₙ ≈ qₙ
——————————————————————————————————————————————————————————
 Γ ⊢ g @α₁ … @αₘ p₁ … pₙ = e ≈ g @β₁ … @βₘ q₁ … qₙ = f

where xᵢ and yᵢ denote the names of the variables bound by the patterns pᵢ and qᵢ respectively.

If the function has an explicit return type annotation, the annotated return typed must be similar as well.

 Γ ∪ { α₁ ↦ β₁, …, αₘ ↦ βₘ, x₁ ↦ y₁, …, xₙ ↦ yₙ } ⊢ e ≈ f
 Γ ∪ { α₁ ↦ β₁, …, αₘ ↦ βₘ } ⊢ p₁ ≈ q₁, …,
 Γ ∪ { α₁ ↦ β₁, …, αₘ ↦ βₘ } ⊢ pₙ ≈ qₙ,
 Γ ∪ { α₁ ↦ β₁, …, αₘ ↦ βₘ } ⊢ τ ≈ τ',
——————————————————————————————————————————————————————————
 Γ ⊢ g @α₁ … @αₘ p₁ … pₙ :: τ = e ≈ g @β₁ … @βₘ q₁ … qₙ :: τ' = f

Function declarations refer to the types their argument and return type annotations refer to as well as the references of their right-hand side except for the (type) variables bound by the function's (type) arguments.

Function declarations can be parsed.

Applies the given type substitution to the right-hand side of a function declaration.

Applies the given expression substitution to the right-hand side of a function declaration.