typerbole-0.0.0.5: A typeystems library with exaggerated claims

Calculi.Lambda.Cube.Polymorphic.Unification

Description

Module containing functions related to solving and unifying polymorphic type expressions.

Synopsis

# Unification related functions

Arguments

 :: (Polymorphic t, p ~ PolyType t, DynGraph gr) => t The first type expression -> t The second type expression -> Either [SubsErr gr t p] [(t, p)] The result from trying to unify both type expressions.

This module's namesake function.

Unification is an important step of typechecking polymorphic lambda calculi, taking two type expressions and computing their differences to produce a sequence of substitutions needed to make both type expressions equivalent.

This implementation computes a list of substitutions with the substitutions to be applied first at the end of the list and the ones to be applied last at the beginning. This is an artifact of how the reordering of the substitutions works and can be remedied with a reverse if needed.

### Behaviour

• Unifying two compatable type expressions

>>> unify (forall a. a) (A → B)
Right [(A → B, a)]

>>> unify (forall a b c. a → (b → c) → a) (forall x. x → (I → x) → G)
Right [(G, a), (G, c), (G, x), (I, b)]

• Unifying incompatable type expressions yeilds errors.

>>> unify (A) (B)
Left [SubsMismatch A B]

• Unifying a poly type with a type expression that contains that poly type yeilds a cyclic substitution error.

>>> unify (a) (F a)
Left [CyclicSubstitution (mkGraph [(2,(F a))] [(2,2,(a))])]]
-- The above is a graph showing the cycle of (F a) trying to substitute it's own poly type (a)

• Unifying equivalent type expressions yeilds empty lists.

>>> unify (forall a. a → C) (forall x. x → C)
Right []

>>> unify (X → Y) (X → Y)
Right []


unifyGr :: forall t p. (Polymorphic t, p ~ PolyType t) => t -> t -> Either [SubsErr Gr t p] [(t, p)] Source #

unify with Gr as the instance for DynGraph.

(⊑) :: Polymorphic t => t -> t -> Bool infix 4 Source #

Type ordering operator, true if the second argument is more specific or equal to the first.

### Behaviour

• A type expression with poly types being ordered against one without them.

>>> (∀ a. a) ⊑ (X → Y)
True

• A type expression being ordered against itself, displaying reflexivity.

>>> (X → X) ⊑ (X → X)
True

• All type expressions are more specific than a type expression of just a single (bound or unbound) poly type.

>>> (a) ⊑ (a)
True

>>> (a) ⊑ (b)
True

>>> (a) ⊑ (X)
True

>>> (a) ⊑ (X → Y)
True


etc.

(\<) :: Polymorphic t => t -> t -> Bool infix 4 Source #

Non-unicode ⊑.

hasSubstitutions :: forall t p. (Polymorphic t, p ~ PolyType t) => t -> t -> Bool Source #

Test to see if two types have valid substitutions between eachother.

applyAllSubs :: forall gr t p. (Polymorphic t, p ~ PolyType t, DynGraph gr) => [(t, p)] -> Either [SubsErr gr t p] (t -> t) Source #

Validate substitutions and fold them into a single substitution function.

applyAllSubsGr :: (Polymorphic t, p ~ PolyType t) => [(t, p)] -> Either [SubsErr Gr t p] (t -> t) Source #

applyAllSubs using fgl's Gr.

unvalidatedApplyAllSubs :: (Polymorphic t, p ~ PolyType t) => [(t, p)] -> t -> t Source #

Without validating if the substitutions are consistent, fold them into a single function that applies all substitutions to a given type expression.

Arguments

 :: (Polymorphic t, p ~ PolyType t) => [Substitution t p] The list of mixed (see Substitution) substitutions. -> [(t, p)] The resulting list of substitutions

Given a list of substitutions, resolve all the mutual substitutions and return a list of substitutions in the form (t, p).

# Substitution validation

## Substitution error datatypes

data SubsErr gr t p Source #

Errors in poly type substitution.

Constructors

 MultipleSubstitutions (ConflictTree t p) A ConflictTree of substitutions leading to p CyclicSubstitution (gr t p) There is a cycle of substitutions. SubsMismatch t t A substitution between two incompatable type expressions was attempted. (i.e. substitutions (X) (Y → Y))

Instances

type ConflictTree t p = ([Tree (t, [p])], t) Source #

A substitution conflict's root, with a tree of types substituting variables as the first element  and the second element being the type where these clashing substitutions converge.

1
to be read that the first element of the tuple is a forest of substitutions leading the final type expression with a substitution conflict.

TODO: Put a diagram here instead.

## Validation and analysis functions

substitutionGraph :: forall gr t p. (Polymorphic t, p ~ PolyType t, DynGraph gr) => [(t, p)] -> Either [SubsErr gr t p] (gr t p) Source #

Function that builds a graph representing valid substitutions or reports any part of the graph's structure that would make the substitutions invalid.

substitutionGraphGr :: forall t p. (Polymorphic t, p ~ PolyType t) => [(t, p)] -> Either [SubsErr Gr t p] (Gr t p) Source #

substitutionGraph using fgl's Gr.

Arguments

 :: (Polymorphic t, p ~ PolyType t, Ord p, DynGraph gr) => [(t, p)] A list of substitutions -> NodeMapM t p gr [SubsErr gr t p] A nodemap monadic action where the graph's edges are substitutions and the nodes are type expressions.

A version of substitutionGraph that works within fgl's NodeMap state monad.

topsortSubs :: forall gr t p. (DynGraph gr, Polymorphic t, p ~ PolyType t) => [(t, p)] -> Either [SubsErr gr t p] [(t, p)] Source #

For a given list of substitutions, either find and report inconsistencies through SubsErr or compute a topsort by order of substitution such that for a list of substitutions [a, b, c] c should be applied, then b, then a.

This backward application is a product of how the graph used to compute the reordering is notated and how topsorting is ordered. In this graph for nodes N, M and egde label p, N --p-> M notates that all instances of p in M will be substituted by N. In regular topsort this means that N will preceed M in the list, but this doesn't make sense when we topsort to tuples of the form (N, p).

topsortSubsG :: forall gr t p. Graph gr => gr t p -> [(t, p)] Source #

A version of topsortSubs that takes an already generated graph rather than building it's own.

If given a graph with cycles or nodes with 2 or more inward edges of the same label then there's no garuntee that the substitutions will be applied correctly.

occursCheck :: forall gr t p. (DynGraph gr, Ord p, Ord t) => gr t p -> [SubsErr gr t p] Source #

From a graph representing substitutions of variables p in terms t, where edges represent the origin node replacing the variable represented by the edge label in the target node.

e.g. The edge (N, (x -> x), x) corresponds to replacing all instances of the variable x in (x -> x) with N.

conflicts :: (DynGraph gr, Ord p, Ord t) => gr t p -> [(p, Context t p)] Source #

Find all contexts with non-unique inward labels, paired with each label that wasn't unique.