symantic-6.3.3.20190614: 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 # 
Instance details

Defined in Language.Symantic.Typing.Unify

Methods

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

show :: Subst src vs -> String #

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

Semigroup (Subst src vs) Source # 
Instance details

Defined in Language.Symantic.Typing.Unify

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 # 
Instance details

Defined in Language.Symantic.Typing.Unify

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 # 
Instance details

Defined in Language.Symantic.Typing.Unify

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 #

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 # 
Instance details

Defined in Language.Symantic.Typing.Unify

Methods

substVarUnsafe :: (src0 ~ SourceOf (Types src vs ts), vs0 ~ VarsOf (Types src vs ts)) => Var src0 vs0 v -> Type src0 vs0 v -> Types src vs ts -> Types src vs ts Source #

subst :: (src0 ~ SourceOf (Types src vs ts), vs0 ~ VarsOf (Types src vs ts)) => Subst src0 vs0 -> Types src vs ts -> Types src vs ts Source #

Substable (Type src vs t) Source # 
Instance details

Defined in Language.Symantic.Typing.Unify

Methods

substVarUnsafe :: (src0 ~ SourceOf (Type src vs t), vs0 ~ VarsOf (Type src vs t)) => Var src0 vs0 v -> Type src0 vs0 v -> Type src vs t -> Type src vs t Source #

subst :: (src0 ~ SourceOf (Type src vs t), vs0 ~ VarsOf (Type src vs t)) => Subst src0 vs0 -> Type src vs t -> Type 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 # 
Instance details

Defined in Language.Symantic.Typing.Unify

Methods

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

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

Source src => Show (Error_Unify src) Source # 
Instance details

Defined in Language.Symantic.Typing.Unify

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 # 
Instance details

Defined in Language.Symantic.Typing.Unify

Methods

errorInj :: Con_Kind src -> Error_Unify src #

ErrorInj (Error_Unify src) (Error_Unify src) Source # 
Instance details

Defined in Language.Symantic.Typing.Unify

Methods

errorInj :: Error_Unify src -> Error_Unify src #

ErrorInj (Error_Unify src) (Error_Beta src) Source # 
Instance details

Defined in Language.Symantic.Compiling.Beta

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 :: ki) (y :: ki) 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.