Top-1.7: Constraint solving framework employed by the Helium Compiler.

Safe HaskellSafe-Infered

Top.Types.Quantification

Contents

Description

Universal and existential quantification of types

Synopsis

Quantification

Universal quantification

generalize :: (Substitutable context, Substitutable a) => context -> a -> Forall aSource

Existential quantification

close :: HasSkolems a => [Int] -> a -> Exists aSource

Skolemization

class HasSkolems a whereSource

Methods

allSkolems :: a -> [Int]Source

changeSkolems :: [(Int, Tp)] -> a -> aSource

Instances

Pretty printing

class Show a => ShowQuantors a whereSource

This class can deal with the pretty printing of (possibly nested) quantifiers.

variableList :: [String]Source

List of unique identifiers.(a, b, .., z, a1, b1 .., z1, a2, ..)