Top.Types.Synonym

This module contains type synonyms to represent type synonyms. A collection of type synonyms can always be ordered, since (mutually) recursive type synonyms are not permitted. The ordering of type synonyms must be determined to find a minimal number of unfold steps to make two types syntactically equivalent.

Type synonyms

type TypeSynonyms = Map String (Int, Tps -> Tp)

A (unordered) collection of type synonyms is represented by a finite map of strings (the name of the type synonym) to pairs that have an int (the number of arguments of the type synonym) and a function.

type TypeSynonymOrdering = Map String Int

An ordering of type synonyms maps a name of a type synonym to a position in the ordering.

type OrderedTypeSynonyms = (TypeSynonymOrdering, TypeSynonyms)

An (unordered) collection of type synonyms, together with an ordering.

Utility functions

noOrderedTypeSynonyms :: OrderedTypeSynonyms

An empty collection of ordered type synonyms.

stringAsTypeSynonym :: OrderedTypeSynonyms

A string is a list of characters

getTypeSynonymOrdering :: TypeSynonyms -> (TypeSynonymOrdering, [[String]])

Order a collection of type synonyms, and return this ordering paired with sets of mutually recursive type synonyms that are detected.

isPhantomTypeSynonym :: OrderedTypeSynonyms -> String -> Bool

Expansion of a type

expandType :: TypeSynonyms -> Tp -> Tp

Fully expand a type in a recursive way.

expandTypeConstructor :: TypeSynonyms -> Tp -> Tp

Fully expand the top-level type constructor.

expandToplevelTC :: OrderedTypeSynonyms -> Tp -> Maybe Tp

Fully expand the top-level type constructor.

expandTypeConstructorOneStep :: TypeSynonyms -> Tp -> Maybe Tp

Try to expand the top-level type constructor one step.

expandOneStepOrdered :: OrderedTypeSynonyms -> (Tp, Tp) -> Maybe (Tp, Tp)

Try to expand the top-level type constructor of one of the two paired Top.Types. If both top-level type constructors can be expanded, then the type synonym thast appears first in the ordering is expanded.