License	BSD-3-Clause
Safe Haskell	None
Language	Haskell2010

Swarm.Effect.Unify.Naive

Description

unification. Uses a simple but expensive-to-maintain invariant on substitutions, and returns a substitution from unification which must then be composed with the substitution being tracked.

Not used in Swarm, and also unmaintained (e.g. Swarm.Effect.Unify.Fast now supports expanding type aliases + recursive types; this module does not). It's still here just for testing/comparison.

Synopsis

class Substitutes n b a where
- subst :: Subst n b -> a -> a
(@@) :: (Ord n, Substitutes n a a) => Subst n a -> Subst n a -> Subst n a
compose :: (Ord n, Substitutes n a a, Foldable t) => t (Subst n a) -> Subst n a
newtype UnificationC (m :: Type -> Type) a = UnificationC {
- unUnificationC :: StateC (Subst IntVar UType) (StateC FreshVarCounter (ThrowC UnificationError m)) a
}
newtype FreshVarCounter = FreshVarCounter {
- getFreshVarCounter :: Int
}
runUnification :: forall (sig :: (Type -> Type) -> Type -> Type) m a. Algebra sig m => UnificationC m a -> m (Either UnificationError a)
unify :: forall (sig :: (Type -> Type) -> Type -> Type) m. Has (Throw UnificationError) sig m => UType -> UType -> m (Subst IntVar UType)
unifyF :: forall (sig :: (Type -> Type) -> Type -> Type) m. Has (Throw UnificationError) sig m => TypeF UType -> TypeF UType -> m (Subst IntVar UType)

Documentation

class Substitutes n b a where Source #

Class of things supporting substitution. Substitutes n b a means that we can apply a substitution of type Subst n b to a value of type a, replacing all the free names of type n inside the a with values of type b, resulting in a new value of type a.

Methods

subst :: Subst n b -> a -> a Source #

Instances

Instances details

(Show n, Ord n, Functor f) => Substitutes n (Free f n) (Free f n) Source #	We can perform substitution on terms built up as the free monad over a structure functor `f`.
Instance details Defined in Swarm.Effect.Unify.Naive Methods subst :: Subst n (Free f n) -> Free f n -> Free f n Source #

(@@) :: (Ord n, Substitutes n a a) => Subst n a -> Subst n a -> Subst n a Source #

Compose two substitutions. Applying s1 @@ s2 is the same as applying first s2, then s1; that is, semantically, composition of substitutions corresponds exactly to function composition when they are considered as functions on terms.

As one would expect, composition is associative and has idS as its identity.

compose :: (Ord n, Substitutes n a a, Foldable t) => t (Subst n a) -> Subst n a Source #

Compose a whole container of substitutions. For example, compose [s1, s2, s3] = s1 @@ s2 @@ s3.

newtype UnificationC (m :: Type -> Type) a Source #

Carrier type for unification: we maintain a current substitution, a counter for generating fresh unification variables, and can throw unification errors.

Constructors

UnificationC
Fields unUnificationC :: StateC (Subst IntVar UType) (StateC FreshVarCounter (ThrowC UnificationError m)) a

Instances

Instances details

MonadIO m => MonadIO (UnificationC m) Source #
Instance details Defined in Swarm.Effect.Unify.Naive Methods liftIO :: IO a -> UnificationC m a #
(Alternative m, Monad m) => Alternative (UnificationC m) Source #
Instance details Defined in Swarm.Effect.Unify.Naive Methods empty :: UnificationC m a # (<\|>) :: UnificationC m a -> UnificationC m a -> UnificationC m a # some :: UnificationC m a -> UnificationC m [a] # many :: UnificationC m a -> UnificationC m [a] #
Monad m => Applicative (UnificationC m) Source #
Instance details Defined in Swarm.Effect.Unify.Naive Methods pure :: a -> UnificationC m a # (<>) :: UnificationC m (a -> b) -> UnificationC m a -> UnificationC m b # liftA2 :: (a -> b -> c) -> UnificationC m a -> UnificationC m b -> UnificationC m c # (>) :: UnificationC m a -> UnificationC m b -> UnificationC m b # (<*) :: UnificationC m a -> UnificationC m b -> UnificationC m a #
Functor m => Functor (UnificationC m) Source #
Instance details Defined in Swarm.Effect.Unify.Naive Methods fmap :: (a -> b) -> UnificationC m a -> UnificationC m b # (<$) :: a -> UnificationC m b -> UnificationC m a #
Monad m => Monad (UnificationC m) Source #
Instance details Defined in Swarm.Effect.Unify.Naive Methods (>>=) :: UnificationC m a -> (a -> UnificationC m b) -> UnificationC m b # (>>) :: UnificationC m a -> UnificationC m b -> UnificationC m b # return :: a -> UnificationC m a #
Algebra sig m => Algebra (Unification :+: sig) (UnificationC m) Source #	Naive implementation of the `Unification` effect in terms of the `UnificationC` carrier. We maintain an invariant on the current `Subst` that map keys never show up in any of the values. For example, we could have `{x -> a+5, y -> 5}` but not `{x -> a+y, y -> 5}`.
Instance details Defined in Swarm.Effect.Unify.Naive Methods alg :: forall ctx (n :: Type -> Type) a. Functor ctx => Handler ctx n (UnificationC m) -> (Unification :+: sig) n a -> ctx () -> UnificationC m (ctx a) #

newtype FreshVarCounter Source #

Counter for generating fresh unification variables.

Constructors

FreshVarCounter
Fields getFreshVarCounter :: Int

Instances

Instances details

Enum FreshVarCounter Source #
Instance details Defined in Swarm.Effect.Unify.Naive Methods succ :: FreshVarCounter -> FreshVarCounter # pred :: FreshVarCounter -> FreshVarCounter # toEnum :: Int -> FreshVarCounter # fromEnum :: FreshVarCounter -> Int # enumFrom :: FreshVarCounter -> [FreshVarCounter] # enumFromThen :: FreshVarCounter -> FreshVarCounter -> [FreshVarCounter] # enumFromTo :: FreshVarCounter -> FreshVarCounter -> [FreshVarCounter] # enumFromThenTo :: FreshVarCounter -> FreshVarCounter -> FreshVarCounter -> [FreshVarCounter] #
Eq FreshVarCounter Source #
Instance details Defined in Swarm.Effect.Unify.Naive Methods (==) :: FreshVarCounter -> FreshVarCounter -> Bool # (/=) :: FreshVarCounter -> FreshVarCounter -> Bool #
Ord FreshVarCounter Source #
Instance details Defined in Swarm.Effect.Unify.Naive Methods compare :: FreshVarCounter -> FreshVarCounter -> Ordering # (<) :: FreshVarCounter -> FreshVarCounter -> Bool # (<=) :: FreshVarCounter -> FreshVarCounter -> Bool # (>) :: FreshVarCounter -> FreshVarCounter -> Bool # (>=) :: FreshVarCounter -> FreshVarCounter -> Bool # max :: FreshVarCounter -> FreshVarCounter -> FreshVarCounter # min :: FreshVarCounter -> FreshVarCounter -> FreshVarCounter #

runUnification :: forall (sig :: (Type -> Type) -> Type -> Type) m a. Algebra sig m => UnificationC m a -> m (Either UnificationError a) Source #

Run a Unification effect via the UnificationC carrier.

unify :: forall (sig :: (Type -> Type) -> Type -> Type) m. Has (Throw UnificationError) sig m => UType -> UType -> m (Subst IntVar UType) Source #

Unify two types and return the mgu, i.e. the smallest substitution which makes them equal.

unifyF :: forall (sig :: (Type -> Type) -> Type -> Type) m. Has (Throw UnificationError) sig m => TypeF UType -> TypeF UType -> m (Subst IntVar UType) Source #

Unify two non-variable terms and return an mgu, i.e. the smallest substitution which makes them equal.