Safe Haskell | None |
---|---|
Language | Haskell2010 |
- class (Ord (PolyType t), SimpleType t) => Polymorphic t where
- data Substitution t p
- = Mutual p p
- | Substitution t p
- areAlphaEquivalent :: forall t. Polymorphic t => t -> t -> Bool
- (≣) :: Polymorphic t => t -> t -> Bool
- (\-/) :: Polymorphic t => PolyType t -> t -> t
- generalise :: forall t. Polymorphic t => Set t -> t -> t
- generalise' :: Polymorphic t => t -> t
- polytypesOf :: Polymorphic t => t -> Set t
- boundPolytypesOf :: Polymorphic t => t -> Set t
- monotypesOf :: Polymorphic t => t -> Set t
- isPolyType :: Polymorphic t => t -> Bool
- data SubsContext t p = SubsContext {}
- type SubsContext' t = SubsContext t (PolyType t)
- subsMade :: forall t p t. Lens (SubsContext t p) (SubsContext t p) (Map p t) (Map p t)
- tape :: forall t p. Lens' (SubsContext t p) [p]
Typeclass for Polymorphic Typesystems
class (Ord (PolyType t), SimpleType t) => Polymorphic t where Source #
Class of typesystems that exhibit polymorphism.
The representation of a poly type, also reffered to as a type variable.
substitutions :: t -> t -> Either [(t, t)] [Substitution t (PolyType t)] Source #
Find the substitutions between two type expressions. If there's a mismatch in structure then report the values passed as a Left value.
Behaviour
A substitution of a poly type "a" for mono type "X"
>>>
substitutions (X) (a)
Right [Substitution (X) (a)]
Two type expressions have substitutions between eachother.
>>>
substitutions (a → B) (X → b)
Right [Substitution (X) (a), Substitution (B) (b)]A mutual substitution between two poly types.
>>>
substitutions (a) (b)
Right [Mutual (a) (b)]Mismatches in structure.
>>>
substitutions (X) (Y)
Left [(X, Y)]>>>
substitutions (C → x C) (x C)
Left [(C → x C, x C)]
applySubstitution :: t -> PolyType t -> t -> t Source #
Substitution application, given one type expression substituting a poly type and a target type expression, substitute all instances of the poly type in the target type expression with the type expression substituting it.
Behaviour
Substituting all instance of "a" with "X"
>>>
applySubstitution X a (∀ a b. a → b → a)
(∀ b. X → b → X)@
Substitution application in a type expression with a type constructor.
>>>
applySubstitution (X → Y) x (M x)
(M (X → Y))Applying a substitution to a type expression that doesn't contain the poly type being substituted
>>>
applySubstitution Y x (M Q)
(M Q)
quantify :: PolyType t -> t -> t Source #
Quantify instances of a poly type in a type expression.
Behaviour
Quantifying a poly type that appears in a type expression.
>>>
quantify a (a → X)
(∀ a. a → X)
Quantifying a poly type that doesn't appear in a type expression
>>>
quantify a (b → X)
(∀ a. b → X)
poly :: PolyType t -> t Source #
Polymorphic constructor synonym, as many implementations will have a constructor along the lines of "Poly p".
polytypesOf :: t -> Set t Source #
Function that retrives all the poly types in a type, quantified or not.
Behaviour
Type expression with some of it's poly types quantified.
>>>
polytypesOf (∀ a b. a → b → c d))
Set.fromList [a, b, c, d]
Type expression with no quantified poly types.
>>>
polytypesOf (a → b → c)
Set.fromList [a, b, c]Type expression with no unquantified poly types.
>>>
polytypesOf (∀ c. X → c)
Set.singleton (c)
quantifiedOf :: t -> Set t Source #
Function that retrives all the quantified poly types in a type expression.
Behaviour
Type expression with some of it's poly types quantified.
>>>
quantifiedOf (∀ a b. a → b → c d))
Set.fromList [a, b]
Type expression with no quantified poly types.
>>>
quantifiedOf (a → b → c)
Set.emptyType expression with no unquantified poly types.
>>>
quantifiedOf (∀ c. X → c)
Set.singleton (c)
(Ord m, Ord p) => Polymorphic (SystemF m p) Source # | |
(Ord m, Ord p, Ord k) => Polymorphic (SystemFOmega m p (Maybe k)) Source # | |
data Substitution t p Source #
Datatype describing possible substitutions found by the substitutions
Polymorphic
typeclass method.
Mutual p p | Two equivalent polytypes that could substitute eachother. |
Substitution t p | A substitution of type expression |
Notation and related functions
areAlphaEquivalent :: forall t. Polymorphic t => t -> t -> Bool Source #
Check if two types are equivalent, where equivalence is defined as the substitutions being made being symbolically identical, where binds and poly types appear in the same place but may have different names (this is Alpha Equivalence).
>>>
areAlphaEquivalent (∀ a. X → a) (∀ z. X → z)
True
>>>
areAlphaEquivalent (M → X) (M → X)
True
>>>
areAlphaEquivalent (∀ a. a) (∀ z. z → z)
False
(≣) :: Polymorphic t => t -> t -> Bool infix 4 Source #
Infix areAlphaEquivalent
(\-/) :: Polymorphic t => PolyType t -> t -> t infixr 6 Source #
Infix quantify
, looks a bit like ∀
but doesn't interfere with unicode syntax extensions.
generalise :: forall t. Polymorphic t => Set t -> t -> t Source #
Quantify every free polytype in a type expression, excluding a set of polytypes to not quantify.
>>>
generalise Set.empty (x → y)
(∀ x y. x → y)
>>>
generalise (Set.fromList [a, b]) (a → b → c)
(∀ c. a → b → c)
generalise' :: Polymorphic t => t -> t Source #
generalise
but with an empty exclusion set.
polytypesOf :: Polymorphic t => t -> Set t Source #
Function that retrives all the poly types in a type, quantified or not.
Behaviour
Type expression with some of it's poly types quantified.
>>>
polytypesOf (∀ a b. a → b → c d))
Set.fromList [a, b, c, d]
Type expression with no quantified poly types.
>>>
polytypesOf (a → b → c)
Set.fromList [a, b, c]Type expression with no unquantified poly types.
>>>
polytypesOf (∀ c. X → c)
Set.singleton (c)
boundPolytypesOf :: Polymorphic t => t -> Set t Source #
Bound polytypes of an expression.
monotypesOf :: Polymorphic t => t -> Set t Source #
Monotypes of a type expression.
isPolyType :: Polymorphic t => t -> Bool Source #
Tests if a type expression is a base poly type.
>>>
isPolyType (∀ a. a)
False
>>>
isPolyType (a)
True
>>>
isPolyType (b → c)
False
Typechecking context
type SubsContext' t = SubsContext t (PolyType t) Source #
SubsContext
but assumes the poly type representation of t
is the second argument.
SubsContext lenses
subsMade :: forall t p t. Lens (SubsContext t p) (SubsContext t p) (Map p t) (Map p t) Source #
tape :: forall t p. Lens' (SubsContext t p) [p] Source #