License	BSD-3-Clause
Safe Haskell	None
Language	Haskell2010

Swarm.Effect.Unify

Description

computations that support doing unification. The intention is for code needing unification to use the operations defined in this module, and then import Fast to dispatch the Unification effects.

Synopsis

data Unification (m :: Type -> Type) k where
- Unify :: forall (m :: Type -> Type). UType -> UType -> Unification m (Either UnificationError UType)
- ApplyBindings :: forall (m :: Type -> Type). UType -> Unification m (Free TypeF IntVar)
- FreshIntVar :: forall (m :: Type -> Type). Unification m IntVar
- FreeUVars :: forall (m :: Type -> Type). UType -> Unification m (Set IntVar)
(=:=) :: forall (sig :: (Type -> Type) -> Type -> Type) m. Has Unification sig m => UType -> UType -> m (Either UnificationError UType)
applyBindings :: forall (sig :: (Type -> Type) -> Type -> Type) m. Has Unification sig m => UType -> m UType
freeUVars :: forall (sig :: (Type -> Type) -> Type -> Type) m. Has Unification sig m => UType -> m (Set IntVar)
freshIntVar :: forall (sig :: (Type -> Type) -> Type -> Type) m. Has Unification sig m => m IntVar
data UnificationError where
- Infinite :: IntVar -> UType -> UnificationError
- UnifyErr :: TypeF UType -> TypeF UType -> UnificationError
- UndefinedUserType :: UType -> UnificationError
- UnexpandedRecTy :: TypeF UType -> UnificationError

Documentation

data Unification (m :: Type -> Type) k where Source #

Data type representing available unification operations.

Constructors

Unify :: forall (m :: Type -> Type). UType -> UType -> Unification m (Either UnificationError UType)
ApplyBindings :: forall (m :: Type -> Type). UType -> Unification m (Free TypeF IntVar)
FreshIntVar :: forall (m :: Type -> Type). Unification m IntVar
FreeUVars :: forall (m :: Type -> Type). UType -> Unification m (Set IntVar)

Instances

Instances details

(Algebra sig m, Has (Reader TDCtx) sig m) => Algebra (Unification :+: sig) (UnificationC m) Source #	Implementation of the `Unification` effect in terms of the `UnificationC` carrier.
Instance details Defined in Swarm.Effect.Unify.Fast Methods alg :: forall ctx (n :: Type -> Type) a. Functor ctx => Handler ctx n (UnificationC m) -> (Unification :+: sig) n a -> ctx () -> UnificationC m (ctx 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) #

(=:=) :: forall (sig :: (Type -> Type) -> Type -> Type) m. Has Unification sig m => UType -> UType -> m (Either UnificationError UType) Source #

Unify two types, returning a type equal to both, or a UnificationError if the types definitely do not unify.

applyBindings :: forall (sig :: (Type -> Type) -> Type -> Type) m. Has Unification sig m => UType -> m UType Source #

Substitute for all the unification variables that are currently bound. It is guaranteed that any unification variables remaining in the result are not currently bound, i.e. we have learned no information about them.

freeUVars :: forall (sig :: (Type -> Type) -> Type -> Type) m. Has Unification sig m => UType -> m (Set IntVar) Source #

Compute the set of free unification variables of a type (after substituting away any which are already bound).

freshIntVar :: forall (sig :: (Type -> Type) -> Type -> Type) m. Has Unification sig m => m IntVar Source #

Generate a fresh unification variable.

data UnificationError where Source #

An error that occurred while running the unifier.

Constructors

Infinite :: IntVar -> UType -> UnificationError	Occurs check failure, i.e. the solution to some unification equations was an infinite term.
UnifyErr :: TypeF UType -> TypeF UType -> UnificationError	Mismatch error between the given terms.
UndefinedUserType :: UType -> UnificationError	Encountered an undefined/unknown type constructor.
UnexpandedRecTy :: TypeF UType -> UnificationError	Encountered an unexpanded recursive type in unifyF. This should never happen.

Instances

Instances details

Show UnificationError Source #
Instance details Defined in Swarm.Effect.Unify Methods showsPrec :: Int -> UnificationError -> ShowS # show :: UnificationError -> String # showList :: [UnificationError] -> ShowS #
PrettyPrec UnificationError Source #
Instance details Defined in Swarm.Effect.Unify Methods prettyPrec :: Int -> UnificationError -> Doc ann