Top.Types.Substitution

This module contains a data type to represent (plain) types, some basic functionality for types, and an instance for Show.

Substitutions and substitutables

class Substitution s where

Methods

lookupInt :: Int -> s -> Tp

removeDom :: [Int] -> s -> s

restrictDom :: [Int] -> s -> s

dom :: s -> [Int]

cod :: s -> Tps

Instances

Substitution WrappedSubstitution

Substitution FixpointSubstitution

Substitution MapSubstitution

class Substitutable a where

Methods

(|->) :: Substitution s => s -> a -> a

ftv :: a -> [Int]

Instances

Substitutable Tp

Substitutable Predicate

Substitutable a => Substitutable [a]

Substitutable a => Substitutable (Maybe a)

Substitutable qs => Substitutable (Sigma qs)

Substitutable (Operation m)

Substitutable (Constraint m)

Substitutable (EqualityConstraint info)

Substitutable (PolymorphismConstraint info)

Substitutable (PredicateMap info)

Substitutable (ExtraConstraint info)

(Substitutable a, Substitutable b) => Substitutable (Either a b)

(Substitutable a, Substitutable b) => Substitutable (a, b)

(Substitutable q, Substitutable a) => Substitutable (Qualification q a)

Substitutable a => Substitutable (Quantification q a)

(Substitutable (f info), Substitutable (g info)) => Substitutable (ConstraintSum f g info)

nextFTV :: Substitutable a => a -> Int

The next type variable that is not free (default is zero)

Substitution instances

type MapSubstitution = Map Int Tp

A substitution represented by a finite map.

emptySubst :: MapSubstitution

(@@) :: MapSubstitution -> MapSubstitution -> MapSubstitution

Compose two finite map substitutions: safe. Note for union: bindings in right argument shadow those in the left

(@@@) :: MapSubstitution -> MapSubstitution -> MapSubstitution

Compose two finite map substitutions: quick and dirty!

singleSubstitution :: Int -> Tp -> MapSubstitution

listToSubstitution :: [(Int, Tp)] -> MapSubstitution

newtype FixpointSubstitution

A fixpoint is computed when looking up the target of a type variable in this substitution. Combining two substitutions is cheap, whereas a lookup is more expensive than the normal finite map substitution.

Constructors

FixpointSubstitution (Map Int Tp)

Instances

Substitution FixpointSubstitution

emptyFPS :: FixpointSubstitution

The empty fixpoint substitution

disjointFPS :: FixpointSubstitution -> FixpointSubstitution -> FixpointSubstitution

Combine two fixpoint substitutions that are disjoint

Wrapper for substitutions

wrapSubstitution :: Substitution substitution => substitution -> WrappedSubstitution

data WrappedSubstitution

Constructors

forall a . Substitution a => WrappedSubstitution a (Int -> a -> Tp, [Int] -> a -> a, [Int] -> a -> a, a -> [Int], a -> Tps)

Instances

Substitution WrappedSubstitution

Substitutables instances

freezeFTV :: Substitutable a => a -> a

allTypeVariables :: HasTypes a => a -> [Int]

allTypeConstants :: HasTypes a => a -> [String]