Calculi.Lambda.Cube.Polymorphic

Typeclass for Polymorphic Typesystems

class (Ord (PolyType t), SimpleType t) => Polymorphic t where

Class of typesystems that exhibit polymorphism.

Minimal complete definition

substitutions, applySubstitution, quantify, poly, polytypesOf, quantifiedOf

Associated Types

type PolyType t :: *

The representation of a poly type, also reffered to as a type variable.

Methods

substitutions :: t -> t -> Either [(t, t)] [Substitution t (PolyType t)]

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

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

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

Polymorphic constructor synonym, as many implementations will have a constructor along the lines of "Poly p".

polytypesOf :: t -> Set t

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

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.empty
  

• Type expression with no unquantified poly types.

  >>> quantifiedOf (∀ c. X → c)
  Set.singleton (c)
  

Instances

(Ord m, Ord p) => Polymorphic (SystemF m p)

Associated Types

type PolyType (SystemF m p) :: *

Methods

substitutions :: SystemF m p -> SystemF m p -> Either [(SystemF m p, SystemF m p)] [Substitution (SystemF m p) (PolyType (SystemF m p))]

applySubstitution :: SystemF m p -> PolyType (SystemF m p) -> SystemF m p -> SystemF m p

quantify :: PolyType (SystemF m p) -> SystemF m p -> SystemF m p

poly :: PolyType (SystemF m p) -> SystemF m p

polytypesOf :: SystemF m p -> Set (SystemF m p)

quantifiedOf :: SystemF m p -> Set (SystemF m p)

(Ord m, Ord p, Ord k) => Polymorphic (SystemFOmega m p (Maybe k))

Associated Types

type PolyType (SystemFOmega m p (Maybe k)) :: *

Methods

substitutions :: SystemFOmega m p (Maybe k) -> SystemFOmega m p (Maybe k) -> Either [(SystemFOmega m p (Maybe k), SystemFOmega m p (Maybe k))] [Substitution (SystemFOmega m p (Maybe k)) (PolyType (SystemFOmega m p (Maybe k)))]

applySubstitution :: SystemFOmega m p (Maybe k) -> PolyType (SystemFOmega m p (Maybe k)) -> SystemFOmega m p (Maybe k) -> SystemFOmega m p (Maybe k)

quantify :: PolyType (SystemFOmega m p (Maybe k)) -> SystemFOmega m p (Maybe k) -> SystemFOmega m p (Maybe k)

poly :: PolyType (SystemFOmega m p (Maybe k)) -> SystemFOmega m p (Maybe k)

polytypesOf :: SystemFOmega m p (Maybe k) -> Set (SystemFOmega m p (Maybe k))

quantifiedOf :: SystemFOmega m p (Maybe k) -> Set (SystemFOmega m p (Maybe k))

data Substitution t p

Datatype describing possible substitutions found by the substitutions Polymorphic typeclass method.

Constructors

Mutual p p

Two equivalent polytypes that could substitute eachother.

Substitution t p

A substitution of type expression t over polytype p

Instances

(Eq t, Eq p) => Eq (Substitution t p)

Methods

(==) :: Substitution t p -> Substitution t p -> Bool

(/=) :: Substitution t p -> Substitution t p -> Bool

(Ord t, Ord p) => Ord (Substitution t p)

Methods

compare :: Substitution t p -> Substitution t p -> Ordering

(<) :: Substitution t p -> Substitution t p -> Bool

(<=) :: Substitution t p -> Substitution t p -> Bool

(>) :: Substitution t p -> Substitution t p -> Bool

(>=) :: Substitution t p -> Substitution t p -> Bool

max :: Substitution t p -> Substitution t p -> Substitution t p

min :: Substitution t p -> Substitution t p -> Substitution t p

(Show t, Show p) => Show (Substitution t p)

Methods

showsPrec :: Int -> Substitution t p -> ShowS

show :: Substitution t p -> String

showList :: [Substitution t p] -> ShowS

Notation and related functions

areAlphaEquivalent :: forall t. Polymorphic t => t -> t -> Bool

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

Infix areAlphaEquivalent

(\-/) :: Polymorphic t => PolyType t -> t -> t infixr 6

Infix quantify, looks a bit like ∀ but doesn't interfere with unicode syntax extensions.

generalise :: forall t. Polymorphic t => Set t -> t -> t

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

generalise but with an empty exclusion set.

polytypesOf :: Polymorphic t => t -> Set t

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

Bound polytypes of an expression.

monotypesOf :: Polymorphic t => t -> Set t

Monotypes of a type expression.

isPolyType :: Polymorphic t => t -> Bool

Tests if a type expression is a base poly type.

>>> isPolyType (∀ a. a)
False

>>> isPolyType (a)
True

>>> isPolyType (b → c)
False

Typechecking context

data SubsContext t p

A TypingContext

Constructors

SubsContext

Fields

• _subsMade :: Map p t

  The substitutions made so far, where the key is the poly type that is substituted and the value is what is substituting it.

• _tape :: [p]

  An infinite list of polytypes not present in the who typing context.

Instances

(Eq t, Eq p) => Eq (SubsContext t p)

Methods

(==) :: SubsContext t p -> SubsContext t p -> Bool

(/=) :: SubsContext t p -> SubsContext t p -> Bool

(Ord t, Ord p) => Ord (SubsContext t p)

Methods

compare :: SubsContext t p -> SubsContext t p -> Ordering

(<) :: SubsContext t p -> SubsContext t p -> Bool

(<=) :: SubsContext t p -> SubsContext t p -> Bool

(>) :: SubsContext t p -> SubsContext t p -> Bool

(>=) :: SubsContext t p -> SubsContext t p -> Bool

max :: SubsContext t p -> SubsContext t p -> SubsContext t p

min :: SubsContext t p -> SubsContext t p -> SubsContext t p

(Show t, Show p) => Show (SubsContext t p)

Note: only shows the first 10 elements of the infinte list.

Methods

showsPrec :: Int -> SubsContext t p -> ShowS

show :: SubsContext t p -> String

showList :: [SubsContext t p] -> ShowS

type SubsContext' t = SubsContext t (PolyType t)

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)

tape :: forall t p. Lens' (SubsContext t p) [p]