symantic-6.3.0.20170703: Library for Typed Tagless-Final Higher-Order Composable DSL

Safe HaskellNone
LanguageHaskell2010

Language.Symantic.Typing.Unify

Contents

Synopsis

Type Subst

newtype Subst src vs Source #

Type variable substitution.

WARNING: a Subst MUST be without loops, and fully expanded.

Constructors

Subst (Map IndexVar (VT src vs)) 

Instances

Source src => Show (Subst src vs) Source # 

Methods

showsPrec :: Int -> Subst src vs -> ShowS #

show :: Subst src vs -> String #

showList :: [Subst src vs] -> ShowS #

Semigroup (Subst src vs) Source # 

Methods

(<>) :: Subst src vs -> Subst src vs -> Subst src vs #

sconcat :: NonEmpty (Subst src vs) -> Subst src vs #

stimes :: Integral b => b -> Subst src vs -> Subst src vs #

Monoid (Subst src vs) Source # 

Methods

mempty :: Subst src vs #

mappend :: Subst src vs -> Subst src vs -> Subst src vs #

mconcat :: [Subst src vs] -> Subst src vs #

unionSubst :: Subst src vs -> Subst src vs -> Subst src vs Source #

Unify two Substs.

NOTE: the union is left-biased: in case of duplicate Vars, it keeps the one from the first Subst given.

NOTE: the first Subst given is applied to the second (with subst), this way each Var directly maps to an expanded Type, so that, when using the resulting Subst, there is no need to apply it multiple times until there is no more substitution to be done.

Type VT

data VT src vs Source #

A Var and a Type existentialized over their type index.

Constructors

VT (Var src vs t) (Type src vs t) 

Instances

Source src => Show (VT src vs) Source # 

Methods

showsPrec :: Int -> VT src vs -> ShowS #

show :: VT src vs -> String #

showList :: [VT src vs] -> ShowS #

insertSubst :: Var src vs v -> Type src vs v -> Subst src vs -> Subst src vs Source #

lookupSubst :: Var src vs v -> Subst src vs -> Maybe (Type src vs v) Source #

Class Substable

class Substable a where Source #

Minimal complete definition

substVarUnsafe, subst

Methods

substVarUnsafe :: src ~ SourceOf a => vs ~ VarsOf a => Var src vs v -> Type src vs v -> a -> a Source #

Like substVar, but without the occurence check.

subst :: src ~ SourceOf a => vs ~ VarsOf a => Subst src vs -> a -> a Source #

Substitute all the Vars which have a match in given Subst.

Instances

Substable (Types src vs ts) Source # 

Methods

substVarUnsafe :: ((* ~ src) (SourceOf (Types src vs ts)), ([Type] ~ vs) (VarsOf (Types src vs ts))) => Var kt src vs v -> Type kt src vs v -> Types src vs ts -> Types src vs ts Source #

subst :: ((* ~ src) (SourceOf (Types src vs ts)), ([Type] ~ vs) (VarsOf (Types src vs ts))) => Subst src vs -> Types src vs ts -> Types src vs ts Source #

Substable (Type kt src vs t) Source # 

Methods

substVarUnsafe :: ((* ~ src) (SourceOf (Type kt src vs t)), ([Type] ~ vs) (VarsOf (Type kt src vs t))) => Var kt src vs v -> Type kt src vs v -> Type kt src vs t -> Type kt src vs t Source #

subst :: ((* ~ src) (SourceOf (Type kt src vs t)), ([Type] ~ vs) (VarsOf (Type kt src vs t))) => Subst src vs -> Type kt src vs t -> Type kt src vs t Source #

substVar :: src ~ SourceOf a => vs ~ VarsOf a => Source src => VarOccursIn a => Substable a => Var src vs v -> Type src vs v -> a -> Maybe a Source #

Substitute the given Var by the given Type, returning Nothing if this Type contains the Var (occurence check).

Type Error_Unify

data Error_Unify src Source #

Reasons why two Types cannot be unified.

Constructors

Error_Unify_Var_loop IndexVar (TypeVT src)

occurence check: a Var is unified with a Type which contains this same Var.

Error_Unify_Const_mismatch (TypeVT src) (TypeVT src)

Two TyConsts should be the same, but are different.

Error_Unify_Kind_mismatch (KindK src) (KindK src)

Two Kinds should be the same, but are different.

Error_Unify_Kind (Con_Kind src)

Two Kinds mismatch.

Error_Unify_mismatch (TypeVT src) (TypeVT src)

Cannot unify those two Types.

Instances

Source src => Eq (Error_Unify src) Source # 

Methods

(==) :: Error_Unify src -> Error_Unify src -> Bool #

(/=) :: Error_Unify src -> Error_Unify src -> Bool #

Source src => Show (Error_Unify src) Source # 

Methods

showsPrec :: Int -> Error_Unify src -> ShowS #

show :: Error_Unify src -> String #

showList :: [Error_Unify src] -> ShowS #

ErrorInj (Con_Kind src) (Error_Unify src) Source # 

Methods

errorInj :: Con_Kind src -> Error_Unify src #

ErrorInj (Error_Unify src) (Error_Unify src) Source # 

Methods

errorInj :: Error_Unify src -> Error_Unify src #

ErrorInj (Error_Unify src) (Error_Beta src) # 

Methods

errorInj :: Error_Unify src -> Error_Beta src #

spineTy :: forall src vs t. Source src => SourceInj (TypeVT src) src => Type src vs t -> (TypeT src vs, [TypeT src vs]) Source #

Return the left spine of a Type: the root Type and its Type parameters, from the left to the right.

unifyType :: forall ki x y vs src. SourceInj (TypeVT src) src => ErrorInj (Con_Kind src) (Error_Unify src) => Subst src vs -> Type src vs (x :: ki) -> Type src vs (y :: ki) -> Either (Error_Unify src) (Subst src vs) Source #

Return the most general unification of two Types, when it exists.