nano-js-0.1.0.0: Small Language for Implementing Verification Algorithms

Safe HaskellNone

Language.Nano.Typecheck.Subst

Contents

Synopsis

Substitutions

data RSubst r Source

Substitutions --------------------------------------------------------

Type alias for Map from TVar to Type. Hidden

Constructors

Su (HashMap TVar (RType r)) 

Instances

(Reftable r, Substitutable r (RType r)) => Monoid (RSubst r)

Substitutions form a monoid; not commutative

(Reftable r, PP r) => PP (RSubst r) 

type Subst = RSubst ()Source

toList :: RSubst r -> [(TVar, RType r)]Source

fromList :: [(TVar, RType r)] -> RSubst rSource

Free Type Variables

class Free a whereSource

Substitutions --------------------------------------------------------

Methods

free :: a -> HashSet TVarSource

Instances

Free Fact 
Free a => Free [a] 
Free (RType r) 

Type-class with operations

class Substitutable r a whereSource

Methods

apply :: RSubst r -> a -> aSource

Instances

Substitutable () Fact 
(PP r, Reftable r) => Substitutable r (Bind r) 
(PP r, Reftable r) => Substitutable r (RType r) 
Substitutable r a => Substitutable r [a] 

Unification

unifys :: Subst -> [Type] -> [Type] -> Either String SubstSource