Safe Haskell | None |
---|---|

Language | Haskell2010 |

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

- unify :: forall gr t p. (Polymorphic t, p ~ PolyType t, DynGraph gr) => t -> t -> Either [SubsErr gr t p] [(t, p)]
- unifyGr :: forall t p. (Polymorphic t, p ~ PolyType t) => t -> t -> Either [SubsErr Gr t p] [(t, p)]
- (⊑) :: Polymorphic t => t -> t -> Bool
- (\<) :: Polymorphic t => t -> t -> Bool
- hasSubstitutions :: forall t p. (Polymorphic t, p ~ PolyType t) => t -> t -> Bool
- applyAllSubs :: forall gr t p. (Polymorphic t, p ~ PolyType t, DynGraph gr) => [(t, p)] -> Either [SubsErr gr t p] (t -> t)
- applyAllSubsGr :: (Polymorphic t, p ~ PolyType t) => [(t, p)] -> Either [SubsErr Gr t p] (t -> t)
- unvalidatedApplyAllSubs :: (Polymorphic t, p ~ PolyType t) => [(t, p)] -> t -> t
- resolveMutuals :: forall t p. (Polymorphic t, p ~ PolyType t) => [Substitution t p] -> [(t, p)]
- data SubsErr gr t p
- = MultipleSubstitutions (ConflictTree t p)
- | CyclicSubstitution (gr t p)
- | SubsMismatch t t

- type ConflictTree t p = ([Tree (t, [p])], t)
- substitutionGraph :: forall gr t p. (Polymorphic t, p ~ PolyType t, DynGraph gr) => [(t, p)] -> Either [SubsErr gr t p] (gr t p)
- substitutionGraphGr :: forall t p. (Polymorphic t, p ~ PolyType t) => [(t, p)] -> Either [SubsErr Gr t p] (Gr t p)
- substitutionGraphM :: forall t p gr. (Polymorphic t, p ~ PolyType t, Ord p, DynGraph gr) => [(t, p)] -> NodeMapM t p gr [SubsErr gr t p]
- topsortSubs :: forall gr t p. (DynGraph gr, Polymorphic t, p ~ PolyType t) => [(t, p)] -> Either [SubsErr gr t p] [(t, p)]
- topsortSubsG :: forall gr t p. Graph gr => gr t p -> [(t, p)]
- occursCheck :: forall gr t p. (DynGraph gr, Ord p, Ord t) => gr t p -> [SubsErr gr t p]
- conflicts :: (DynGraph gr, Ord p, Ord t) => gr t p -> [(p, Context t p)]

# Unification related functions

:: (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

`>>>`

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

`>>>`

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

Unifying incompatable type expressions yeilds errors.

`>>>`

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

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

`>>>`

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)`unify (a) (F a)`

Unifying equivalent type expressions yeilds empty lists.

`>>>`

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

`>>>`

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

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

(⊑) :: 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.

`>>>`

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

A type expression being ordered against itself, displaying reflexivity.

`>>>`

True`(X → X) ⊑ (X → X)`

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

`>>>`

True`(a) ⊑ (a)`

`>>>`

True`(a) ⊑ (b)`

`>>>`

True`(a) ⊑ (X)`

`>>>`

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

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.

:: (Polymorphic t, p ~ PolyType t) | |

=> [Substitution t p] | The list of mixed (see |

-> [(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

Errors in poly type substitution.

MultipleSubstitutions (ConflictTree t p) | A |

CyclicSubstitution (gr t p) | There is a cycle of substitutions. |

SubsMismatch t t | A substitution between two incompatable type expressions
was attempted. (i.e. |

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 [1] 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`

.

:: (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`

.