AST.Class.Infer

Documentation

type family InferOf (t :: Knot -> Type) :: Knot -> Type

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)

Defined in AST.Term.App

type InferOf (App e) = ANode (TypeOf e)

type InferOf (Compose Prune t)

Defined in AST.Knot.Prune

type InferOf (Compose Prune t) = InferOf t

type InferOf (Var v t)

Defined in AST.Term.Var

type InferOf (Var v t) = ANode (TypeOf t)

type InferOf (Scheme v t)

Defined in AST.Term.Scheme

type InferOf (Scheme v t) = Flip GTerm t

type InferOf (TypeSig v t)

Defined in AST.Term.TypeSig

type InferOf (TypeSig v t) = InferOf t

type InferOf (FromNom n e)

Defined in AST.Term.Nominal

type InferOf (FromNom n e) = FuncType (TypeOf e)

type InferOf (ToNom n e)

Defined in AST.Term.Nominal

type InferOf (ToNom n e) = NominalInst n (NomVarTypes (TypeOf e))

type InferOf (Let v e)

Defined in AST.Term.Let

type InferOf (Let v e) = InferOf e

type InferOf (Lam v t)

Defined in AST.Term.Lam

type InferOf (Lam v t) = FuncType (TypeOf t)

type InferOf (Scope t k)

Defined in AST.Term.NamelessScope

type InferOf (Scope t k) = FuncType (TypeOf (t k))

type InferOf (ScopeVar t k)

Defined in AST.Term.NamelessScope

type InferOf (ScopeVar t k) = ANode (TypeOf (t k))

type InferOf (Sum a b)

Defined in AST.Class.Infer

type InferOf (Sum a b) = InferOf a

type InferOf (TypedLam v t e)

Defined in AST.Term.TypedLam

type InferOf (TypedLam v t e) = FuncType (TypeOf e)

class (Monad m, KFunctor t) => Infer m t where

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 the m 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.

Minimal complete definition

inferBody

Methods

inferBody :: Tree t (InferChild m k) -> m (Tree t k, Tree (InferOf t) (UVarOf m))

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))

inferContext :: (KNodesConstraint t (Infer m), KNodesConstraint (InferOf t) (Unify m)) => Proxy m -> Proxy t -> Dict (KNodesConstraint t (Infer m), KNodesConstraint (InferOf t) (Unify m))

Instances

(Infer m expr, HasInferredType expr, HasFuncType (TypeOf expr), Unify m (TypeOf expr)) => Infer m (App expr)

Defined in AST.Term.App

Methods

inferBody :: Tree (App expr) (InferChild m k) -> m (Tree (App expr) k, Tree (InferOf (App expr)) (UVarOf m))

inferContext :: Proxy m -> Proxy (App expr) -> Dict (KNodesConstraint (App expr) (Infer m), KNodesConstraint (InferOf (App expr)) (Unify m))

(Unify m (TypeOf expr), HasScope m (ScopeOf expr), VarType v expr, Monad m) => Infer m (Var v expr)

Defined in AST.Term.Var

Methods

inferBody :: Tree (Var v expr) (InferChild m k) -> m (Tree (Var v expr) k, Tree (InferOf (Var v expr)) (UVarOf m))

inferContext :: Proxy m -> Proxy (Var v expr) -> Dict (KNodesConstraint (Var v expr) (Infer m), KNodesConstraint (InferOf (Var v expr)) (Unify m))

(Monad m, HasInferredValue typ, Unify m typ, KTraversable varTypes, KNodesConstraint varTypes (MonadInstantiate m), RTraversable typ, Infer m typ) => Infer m (Scheme varTypes typ)

Defined in AST.Term.Scheme

Methods

inferBody :: Tree (Scheme varTypes typ) (InferChild m k) -> m (Tree (Scheme varTypes typ) k, Tree (InferOf (Scheme varTypes typ)) (UVarOf m))

inferContext :: Proxy m -> Proxy (Scheme varTypes typ) -> Dict (KNodesConstraint (Scheme varTypes typ) (Infer m), KNodesConstraint (InferOf (Scheme varTypes typ)) (Unify m))

(MonadScopeLevel m, HasInferredType term, HasInferredValue (TypeOf term), KTraversable vars, KTraversable (InferOf term), KNodesConstraint (InferOf term) (Unify m), KNodesConstraint vars (MonadInstantiate m), Unify m (TypeOf term), Infer m (TypeOf term), Infer m term) => Infer m (TypeSig vars term)

Defined in AST.Term.TypeSig

Methods

inferBody :: Tree (TypeSig vars term) (InferChild m k) -> m (Tree (TypeSig vars term) k, Tree (InferOf (TypeSig vars term)) (UVarOf m))

inferContext :: Proxy m -> Proxy (TypeSig vars term) -> Dict (KNodesConstraint (TypeSig vars term) (Infer m), KNodesConstraint (InferOf (TypeSig vars term)) (Unify m))

(Infer m expr, HasNominalInst nomId (TypeOf expr), MonadNominals nomId (TypeOf expr) m, KTraversable (NomVarTypes (TypeOf expr)), KNodesConstraint (NomVarTypes (TypeOf expr)) (Unify m), Unify m (TypeOf expr)) => Infer m (FromNom nomId expr)

Defined in AST.Term.Nominal

Methods

inferBody :: Tree (FromNom nomId expr) (InferChild m k) -> m (Tree (FromNom nomId expr) k, Tree (InferOf (FromNom nomId expr)) (UVarOf m))

inferContext :: Proxy m -> Proxy (FromNom nomId expr) -> Dict (KNodesConstraint (FromNom nomId expr) (Infer m), KNodesConstraint (InferOf (FromNom nomId expr)) (Unify m))

(MonadScopeLevel m, MonadNominals nomId (TypeOf expr) m, KTraversable (NomVarTypes (TypeOf expr)), KNodesConstraint (NomVarTypes (TypeOf expr)) (Unify m), Unify m (TypeOf expr), HasInferredType expr, Infer m expr) => Infer m (ToNom nomId expr)

Defined in AST.Term.Nominal

Methods

inferBody :: Tree (ToNom nomId expr) (InferChild m k) -> m (Tree (ToNom nomId expr) k, Tree (InferOf (ToNom nomId expr)) (UVarOf m))

inferContext :: Proxy m -> Proxy (ToNom nomId expr) -> Dict (KNodesConstraint (ToNom nomId expr) (Infer m), KNodesConstraint (InferOf (ToNom nomId expr)) (Unify m))

(MonadScopeLevel m, LocalScopeType v (Tree (GTerm (UVarOf m)) (TypeOf expr)) m, Unify m (TypeOf expr), HasInferredType expr, KNodesConstraint (InferOf expr) (Unify m), KTraversable (InferOf expr), Infer m expr) => Infer m (Let v expr)

Defined in AST.Term.Let

Methods

inferBody :: Tree (Let v expr) (InferChild m k) -> m (Tree (Let v expr) k, Tree (InferOf (Let v expr)) (UVarOf m))

inferContext :: Proxy m -> Proxy (Let v expr) -> Dict (KNodesConstraint (Let v expr) (Infer m), KNodesConstraint (InferOf (Let v expr)) (Unify m))

(Infer m t, Unify m (TypeOf t), HasInferredType t, LocalScopeType v (Tree (UVarOf m) (TypeOf t)) m) => Infer m (Lam v t)

Defined in AST.Term.Lam

Methods

inferBody :: Tree (Lam v t) (InferChild m k) -> m (Tree (Lam v t) k, Tree (InferOf (Lam v t)) (UVarOf m))

inferContext :: Proxy m -> Proxy (Lam v t) -> Dict (KNodesConstraint (Lam v t) (Infer m), KNodesConstraint (InferOf (Lam v t)) (Unify m))

(Infer m t, KPointed (InferOf t), KTraversable (InferOf t)) => Infer m (Compose Prune t)

Defined in AST.Knot.Prune

Methods

inferBody :: Tree (Compose Prune t) (InferChild m k) -> m (Tree (Compose Prune t) k, Tree (InferOf (Compose Prune t)) (UVarOf m))

inferContext :: Proxy m -> Proxy (Compose Prune t) -> Dict (KNodesConstraint (Compose Prune t) (Infer m), KNodesConstraint (InferOf (Compose Prune t)) (Unify m))

(MonadReader env m, HasScopeTypes (UVarOf m) (TypeOf (t k)) env, DeBruijnIndex k, Unify m (TypeOf (t k))) => Infer m (ScopeVar t k)

Defined in AST.Term.NamelessScope

Methods

inferBody :: Tree (ScopeVar t k) (InferChild m k0) -> m (Tree (ScopeVar t k) k0, Tree (InferOf (ScopeVar t k)) (UVarOf m))

inferContext :: Proxy m -> Proxy (ScopeVar t k) -> Dict (KNodesConstraint (ScopeVar t k) (Infer m), KNodesConstraint (InferOf (ScopeVar t k)) (Unify m))

(Infer1 m t, HasInferOf1 t, InferOf1IndexConstraint t ~ DeBruijnIndex, DeBruijnIndex k, Unify m (TypeOf (t k)), MonadReader env m, HasScopeTypes (UVarOf m) (TypeOf (t k)) env, HasInferredType (t k)) => Infer m (Scope t k)

Defined in AST.Term.NamelessScope

Methods

inferBody :: Tree (Scope t k) (InferChild m k0) -> m (Tree (Scope t k) k0, Tree (InferOf (Scope t k)) (UVarOf m))

inferContext :: Proxy m -> Proxy (Scope t k) -> Dict (KNodesConstraint (Scope t k) (Infer m), KNodesConstraint (InferOf (Scope t k)) (Unify m))

(InferOf a ~ InferOf b, Infer m a, Infer m b) => Infer m (Sum a b)

Defined in AST.Class.Infer

Methods

inferBody :: Tree (Sum a b) (InferChild m k) -> m (Tree (Sum a b) k, Tree (InferOf (Sum a b)) (UVarOf m))

inferContext :: Proxy m -> Proxy (Sum a b) -> Dict (KNodesConstraint (Sum a b) (Infer m), KNodesConstraint (InferOf (Sum a b)) (Unify m))

(Infer m t, Infer m e, HasInferredType e, Unify m (TypeOf e), HasChild (InferOf t) (TypeOf e), LocalScopeType v (Tree (UVarOf m) (TypeOf e)) m) => Infer m (TypedLam v t e)

Defined in AST.Term.TypedLam

Methods

inferBody :: Tree (TypedLam v t e) (InferChild m k) -> m (Tree (TypedLam v t e) k, Tree (InferOf (TypedLam v t e)) (UVarOf m))

inferContext :: Proxy m -> Proxy (TypedLam v t e) -> Dict (KNodesConstraint (TypedLam v t e) (Infer m), KNodesConstraint (InferOf (TypedLam v t e)) (Unify m))

Recursive (Infer m)

Defined in AST.Class.Infer

Methods

recurse :: (KNodes k, Infer m k) => Proxy (Infer m k) -> Dict (KNodesConstraint k (Infer m))

newtype InferChild m k t

A Knot containing an inference action.

The caller may modify the scope before invoking the action via localScopeType or localLevel

Constructors

InferChild

Fields

• 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

A Knot containing an inferred child node

Constructors

InferredChild

Fields

• _inRep :: !(k t)

  Inferred node.

  An inferBody implementation needs to place this value in the corresponding child node of the inferred term body

• _inType :: !(Tree (InferOf (GetKnot t)) v)

  The inference result for the child node.

  An inferBody implementation may use it to perform unifications with it.

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)