Safe Haskell	Safe-Inferred
Language	Haskell2010

Hyper.Class.Infer

Synopsis

type family InferOf (t :: HyperType) :: HyperType
class (Monad m, HFunctor t) => Infer m t where
- inferBody :: (t # InferChild m h) -> m (t # h, InferOf t # UVarOf m)
- inferContext :: proxy0 m -> proxy1 t -> Dict (HNodesConstraint t (Infer m), HNodesConstraint (InferOf t) (UnifyGen m))
newtype InferChild m h t = InferChild {
- inferChild :: m (InferredChild (UVarOf m) h t)
}
_InferChild :: forall m h t m h t. Iso (InferChild m h t) (InferChild m h t) (m (InferredChild (UVarOf m) h t)) (m (InferredChild (UVarOf m) h t))
data InferredChild v h t = InferredChild {
- _inRep :: !(h t)
- _inType :: !(InferOf (GetHyperType t) # v)
}
inType :: forall v h t v. Lens (InferredChild v h t) (InferredChild v h t) ((#) (InferOf (GetHyperType t)) v) ((#) (InferOf (GetHyperType t)) v)
inRep :: forall v h t h. Lens (InferredChild v h t) (InferredChild v h t) (h t) (h t)

Documentation

type family InferOf (t :: HyperType) :: HyperType 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

Instances details

type InferOf (App e) Source #
Instance details Defined in Hyper.Syntax.App type InferOf (App e) = ANode (TypeOf e)
type InferOf (Rec1 h) Source #
Instance details Defined in Hyper.Class.Infer type InferOf (Rec1 h) = InferOf h
type InferOf (HCompose Prune t) Source #
Instance details Defined in Hyper.Type.Prune type InferOf (HCompose Prune t) = InferOf t
type InferOf (Lam _1 t) Source #
Instance details Defined in Hyper.Syntax.Lam type InferOf (Lam _1 t) = ANode (TypeOf t)
type InferOf (Let _1 e) Source #
Instance details Defined in Hyper.Syntax.Let type InferOf (Let _1 e) = InferOf e
type InferOf (FromNom _1 e) Source #
Instance details Defined in Hyper.Syntax.Nominal type InferOf (FromNom _1 e) = FuncType (TypeOf e)
type InferOf (ToNom n e) Source #
Instance details Defined in Hyper.Syntax.Nominal type InferOf (ToNom n e) = NominalInst n (NomVarTypes (TypeOf e))
type InferOf (Scheme _1 t) Source #
Instance details Defined in Hyper.Syntax.Scheme type InferOf (Scheme _1 t) = HFlip GTerm t
type InferOf (TypeSig _1 t) Source #
Instance details Defined in Hyper.Syntax.TypeSig type InferOf (TypeSig _1 t) = InferOf t
type InferOf (Var _1 t) Source #
Instance details Defined in Hyper.Syntax.Var type InferOf (Var _1 t) = ANode (TypeOf t)
type InferOf (a :+: _1) Source #
Instance details Defined in Hyper.Class.Infer type InferOf (a :+: _1) = InferOf a
type InferOf (TypedLam _1 _2 e) Source #
Instance details Defined in Hyper.Syntax.TypedLam type InferOf (TypedLam _1 _2 e) = ANode (TypeOf e)
type InferOf (M1 _1 _2 h) Source #
Instance details Defined in Hyper.Class.Infer type InferOf (M1 _1 _2 h) = InferOf h

class (Monad m, HFunctor 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:

HNodesConstraint (InferOf t) (Unify m) - The child nodes of the inferrence can unify in the m Monad
HNodesConstraint 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

Nothing

Methods

inferBody :: (t # InferChild m h) -> m (t # h, InferOf t # UVarOf m) Source #

Infer the body of an expression given the inference actions for its child nodes.

default inferBody :: (Generic1 t, Infer m (Rep1 t), InferOf t ~ InferOf (Rep1 t)) => (t # InferChild m h) -> m (t # h, InferOf t # UVarOf m) Source #

inferContext :: proxy0 m -> proxy1 t -> Dict (HNodesConstraint t (Infer m), HNodesConstraint (InferOf t) (UnifyGen m)) Source #

default inferContext :: (HNodesConstraint t (Infer m), HNodesConstraint (InferOf t) (UnifyGen m)) => proxy0 m -> proxy1 t -> Dict (HNodesConstraint t (Infer m), HNodesConstraint (InferOf t) (UnifyGen m)) Source #

Instances

Instances details

(Infer m expr, HasInferredType expr, HSubset' (TypeOf expr) (FuncType (TypeOf expr)), UnifyGen m (TypeOf expr)) => Infer m (App expr) Source #
Instance details Defined in Hyper.Syntax.App Methods inferBody :: forall (h :: AHyperType -> Type). (App expr # InferChild m h) -> m (App expr # h, InferOf (App expr) # UVarOf m) Source # inferContext :: proxy0 m -> proxy1 (App expr) -> Dict (HNodesConstraint (App expr) (Infer m), HNodesConstraint (InferOf (App expr)) (UnifyGen m)) Source #
Infer m h => Infer m (Rec1 h) Source #
Instance details Defined in Hyper.Class.Infer Methods inferBody :: forall (h0 :: AHyperType -> Type). (Rec1 h # InferChild m h0) -> m (Rec1 h # h0, InferOf (Rec1 h) # UVarOf m) Source # inferContext :: proxy0 m -> proxy1 (Rec1 h) -> Dict (HNodesConstraint (Rec1 h) (Infer m), HNodesConstraint (InferOf (Rec1 h)) (UnifyGen m)) Source #
(Infer m t, HPointed (InferOf t), HTraversable (InferOf t), HNodesConstraint t (HComposeConstraint1 (Infer m) Prune)) => Infer m (HCompose Prune t) Source #
Instance details Defined in Hyper.Type.Prune Methods inferBody :: forall (h :: AHyperType -> Type). (HCompose Prune t # InferChild m h) -> m (HCompose Prune t # h, InferOf (HCompose Prune t) # UVarOf m) Source # inferContext :: proxy0 m -> proxy1 (HCompose Prune t) -> Dict (HNodesConstraint (HCompose Prune t) (Infer m), HNodesConstraint (InferOf (HCompose Prune t)) (UnifyGen m)) Source #
(Infer m t, UnifyGen m (TypeOf t), HSubset' (TypeOf t) (FuncType (TypeOf t)), HasInferredType t, LocalScopeType v (UVarOf m # TypeOf t) m) => Infer m (Lam v t) Source #
Instance details Defined in Hyper.Syntax.Lam Methods inferBody :: forall (h :: AHyperType -> Type). (Lam v t # InferChild m h) -> m (Lam v t # h, InferOf (Lam v t) # UVarOf m) Source # inferContext :: proxy0 m -> proxy1 (Lam v t) -> Dict (HNodesConstraint (Lam v t) (Infer m), HNodesConstraint (InferOf (Lam v t)) (UnifyGen m)) Source #
(MonadScopeLevel m, LocalScopeType v (GTerm (UVarOf m) # TypeOf expr) m, UnifyGen m (TypeOf expr), HasInferredType expr, HNodesConstraint (InferOf expr) (UnifyGen m), HTraversable (InferOf expr), Infer m expr) => Infer m (Let v expr) Source #
Instance details Defined in Hyper.Syntax.Let Methods inferBody :: forall (h :: AHyperType -> Type). (Let v expr # InferChild m h) -> m (Let v expr # h, InferOf (Let v expr) # UVarOf m) Source # inferContext :: proxy0 m -> proxy1 (Let v expr) -> Dict (HNodesConstraint (Let v expr) (Infer m), HNodesConstraint (InferOf (Let v expr)) (UnifyGen m)) Source #
(Infer m expr, HasNominalInst nomId (TypeOf expr), MonadNominals nomId (TypeOf expr) m, HTraversable (NomVarTypes (TypeOf expr)), HNodesConstraint (NomVarTypes (TypeOf expr)) (UnifyGen m), UnifyGen m (TypeOf expr)) => Infer m (FromNom nomId expr) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods inferBody :: forall (h :: AHyperType -> Type). (FromNom nomId expr # InferChild m h) -> m (FromNom nomId expr # h, InferOf (FromNom nomId expr) # UVarOf m) Source # inferContext :: proxy0 m -> proxy1 (FromNom nomId expr) -> Dict (HNodesConstraint (FromNom nomId expr) (Infer m), HNodesConstraint (InferOf (FromNom nomId expr)) (UnifyGen m)) Source #
(MonadScopeLevel m, MonadNominals nomId (TypeOf expr) m, HTraversable (NomVarTypes (TypeOf expr)), HNodesConstraint (NomVarTypes (TypeOf expr)) (UnifyGen m), UnifyGen m (TypeOf expr), HasInferredType expr, Infer m expr) => Infer m (ToNom nomId expr) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods inferBody :: forall (h :: AHyperType -> Type). (ToNom nomId expr # InferChild m h) -> m (ToNom nomId expr # h, InferOf (ToNom nomId expr) # UVarOf m) Source # inferContext :: proxy0 m -> proxy1 (ToNom nomId expr) -> Dict (HNodesConstraint (ToNom nomId expr) (Infer m), HNodesConstraint (InferOf (ToNom nomId expr)) (UnifyGen m)) Source #
(HasInferredValue typ, UnifyGen m typ, HTraversable varTypes, HNodesConstraint varTypes (MonadInstantiate m), Infer m typ) => Infer m (Scheme varTypes typ) Source #
Instance details Defined in Hyper.Syntax.Scheme Methods inferBody :: forall (h :: AHyperType -> Type). (Scheme varTypes typ # InferChild m h) -> m (Scheme varTypes typ # h, InferOf (Scheme varTypes typ) # UVarOf m) Source # inferContext :: proxy0 m -> proxy1 (Scheme varTypes typ) -> Dict (HNodesConstraint (Scheme varTypes typ) (Infer m), HNodesConstraint (InferOf (Scheme varTypes typ)) (UnifyGen m)) Source #
(MonadScopeLevel m, HasInferredType term, HasInferredValue (TypeOf term), HTraversable vars, HTraversable (InferOf term), HNodesConstraint (InferOf term) (UnifyGen m), HNodesConstraint vars (MonadInstantiate m), UnifyGen m (TypeOf term), Infer m (TypeOf term), Infer m term) => Infer m (TypeSig vars term) Source #
Instance details Defined in Hyper.Syntax.TypeSig Methods inferBody :: forall (h :: AHyperType -> Type). (TypeSig vars term # InferChild m h) -> m (TypeSig vars term # h, InferOf (TypeSig vars term) # UVarOf m) Source # inferContext :: proxy0 m -> proxy1 (TypeSig vars term) -> Dict (HNodesConstraint (TypeSig vars term) (Infer m), HNodesConstraint (InferOf (TypeSig vars term)) (UnifyGen m)) Source #
(UnifyGen m (TypeOf expr), HasScope m (ScopeOf expr), VarType v expr, Monad m) => Infer m (Var v expr) Source #
Instance details Defined in Hyper.Syntax.Var Methods inferBody :: forall (h :: AHyperType -> Type). (Var v expr # InferChild m h) -> m (Var v expr # h, InferOf (Var v expr) # UVarOf m) Source # inferContext :: proxy0 m -> proxy1 (Var v expr) -> Dict (HNodesConstraint (Var v expr) (Infer m), HNodesConstraint (InferOf (Var v expr)) (UnifyGen m)) Source #
(InferOf a ~ InferOf b, Infer m a, Infer m b) => Infer m (a :+: b) Source #
Instance details Defined in Hyper.Class.Infer Methods inferBody :: forall (h :: AHyperType -> Type). ((a :+: b) # InferChild m h) -> m ((a :+: b) # h, InferOf (a :+: b) # UVarOf m) Source # inferContext :: proxy0 m -> proxy1 (a :+: b) -> Dict (HNodesConstraint (a :+: b) (Infer m), HNodesConstraint (InferOf (a :+: b)) (UnifyGen m)) Source #
(Infer m t, Infer m e, HasInferredType e, UnifyGen m (TypeOf e), HSubset' (TypeOf e) (FuncType (TypeOf e)), HNodeLens (InferOf t) (TypeOf e), LocalScopeType v (UVarOf m # TypeOf e) m) => Infer m (TypedLam v t e) Source #
Instance details Defined in Hyper.Syntax.TypedLam Methods inferBody :: forall (h :: AHyperType -> Type). (TypedLam v t e # InferChild m h) -> m (TypedLam v t e # h, InferOf (TypedLam v t e) # UVarOf m) Source # inferContext :: proxy0 m -> proxy1 (TypedLam v t e) -> Dict (HNodesConstraint (TypedLam v t e) (Infer m), HNodesConstraint (InferOf (TypedLam v t e)) (UnifyGen m)) Source #
Infer m h => Infer m (M1 i c h) Source #
Instance details Defined in Hyper.Class.Infer Methods inferBody :: forall (h0 :: AHyperType -> Type). (M1 i c h # InferChild m h0) -> m (M1 i c h # h0, InferOf (M1 i c h) # UVarOf m) Source # inferContext :: proxy0 m -> proxy1 (M1 i c h) -> Dict (HNodesConstraint (M1 i c h) (Infer m), HNodesConstraint (InferOf (M1 i c h)) (UnifyGen m)) Source #
Recursive (Infer m) Source #
Instance details Defined in Hyper.Class.Infer Methods recurse :: forall (h :: HyperType) proxy. (HNodes h, Infer m h) => proxy (Infer m h) -> Dict (HNodesConstraint h (Infer m)) Source #

newtype InferChild m h t Source #

A HyperType 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) h t)

_InferChild :: forall m h t m h t. Iso (InferChild m h t) (InferChild m h t) (m (InferredChild (UVarOf m) h t)) (m (InferredChild (UVarOf m) h t)) Source #

data InferredChild v h t Source #

A HyperType containing an inferred child node

Constructors

InferredChild
Fields _inRep :: !(h t) Inferred node. An `inferBody` implementation needs to place this value in the corresponding child node of the inferred term body _inType :: !(InferOf (GetHyperType t) # v) The inference result for the child node. An `inferBody` implementation may use it to perform unifications with it.

inType :: forall v h t v. Lens (InferredChild v h t) (InferredChild v h t) ((#) (InferOf (GetHyperType t)) v) ((#) (InferOf (GetHyperType t)) v) Source #

inRep :: forall v h t h. Lens (InferredChild v h t) (InferredChild v h t) (h t) (h t) Source #