Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- type family InferOf (t :: Knot -> Type) :: Knot -> Type
- class (Monad m, KFunctor t) => Infer m t where
- inferBody :: Tree t (InferChild m k) -> m (Tree t k, Tree (InferOf t) (UVarOf m))
- inferContext :: Proxy m -> Proxy t -> Dict (KNodesConstraint t (Infer m), KNodesConstraint (InferOf t) (Unify m))
- newtype InferChild m k t = InferChild {
- inferChild :: m (InferredChild (UVarOf m) k t)
- _InferChild :: forall m k t m k t. Iso (InferChild m k t) (InferChild m k t) (m (InferredChild (UVarOf m) k t)) (m (InferredChild (UVarOf m) k t))
- data InferredChild v k t = InferredChild {}
- inType :: forall v k t v. Lens (InferredChild v k t) (InferredChild v k t) (Tree (InferOf (GetKnot t)) v) (Tree (InferOf (GetKnot t)) v)
- inRep :: forall v k t k. Lens (InferredChild v k t) (InferredChild v k t) (k t) (k t)
Documentation
type family InferOf (t :: Knot -> Type) :: Knot -> Type Source #
InferOf e
is the inference result of e
.
Most commonly it is an inferred type, using
type instance InferOf MyTerm = ANode MyType
But it may also be other things, for example:
- An inferred value (for types inside terms)
- An inferred type together with a scope
Instances
type InferOf (App e) Source # | |
Defined in AST.Term.App | |
type InferOf (Compose Prune t) Source # | |
Defined in AST.Knot.Prune | |
type InferOf (Var v t) Source # | |
Defined in AST.Term.Var | |
type InferOf (Scheme v t) Source # | |
Defined in AST.Term.Scheme | |
type InferOf (TypeSig v t) Source # | |
Defined in AST.Term.TypeSig | |
type InferOf (FromNom n e) Source # | |
Defined in AST.Term.Nominal | |
type InferOf (ToNom n e) Source # | |
Defined in AST.Term.Nominal | |
type InferOf (Let v e) Source # | |
Defined in AST.Term.Let | |
type InferOf (Lam v t) Source # | |
Defined in AST.Term.Lam | |
type InferOf (Scope t k) Source # | |
Defined in AST.Term.NamelessScope | |
type InferOf (ScopeVar t k) Source # | |
Defined in AST.Term.NamelessScope | |
type InferOf (Sum a b) Source # | |
Defined in AST.Class.Infer | |
type InferOf (TypedLam v t e) Source # | |
Defined in AST.Term.TypedLam |
class (Monad m, KFunctor t) => Infer m t where Source #
Infer m t
enables infer
to perform type-inference for t
in the Monad
m
.
The inferContext
method represents the following constraints on t
:
KNodesConstraint (InferOf t) (Unify m)
- The child nodes of the inferrence can unify in them
Monad
KNodesConstraint t (Infer m)
-Infer m
is also available for child nodes
It replaces context for the Infer
class to avoid UndecidableSuperClasses
.
Instances usually don't need to implement this method as the default implementation works for them,
but infinitely polymorphic trees such as Scope
do need to implement the method,
because the required context is infinite.
inferBody :: Tree t (InferChild m k) -> m (Tree t k, Tree (InferOf t) (UVarOf m)) Source #
Infer the body of an expression given the inference actions for its child nodes.
inferContext :: Proxy m -> Proxy t -> Dict (KNodesConstraint t (Infer m), KNodesConstraint (InferOf t) (Unify m)) Source #
inferContext :: (KNodesConstraint t (Infer m), KNodesConstraint (InferOf t) (Unify m)) => Proxy m -> Proxy t -> Dict (KNodesConstraint t (Infer m), KNodesConstraint (InferOf t) (Unify m)) Source #
Instances
newtype InferChild m k t Source #
A Knot
containing an inference action.
The caller may modify the scope before invoking the action via
localScopeType
or localLevel
InferChild | |
|
_InferChild :: forall m k t m k t. Iso (InferChild m k t) (InferChild m k t) (m (InferredChild (UVarOf m) k t)) (m (InferredChild (UVarOf m) k t)) Source #
inType :: forall v k t v. Lens (InferredChild v k t) (InferredChild v k t) (Tree (InferOf (GetKnot t)) v) (Tree (InferOf (GetKnot t)) v) Source #
inRep :: forall v k t k. Lens (InferredChild v k t) (InferredChild v k t) (k t) (k t) Source #