Safe Haskell	Safe-Inferred
Language	Haskell2010

Hyper.Syntax.Nominal

Description

Nominal (named) types declaration, instantiation, construction, and access.

Synopsis

data NominalDecl typ h = NominalDecl {
- _nParams :: NomVarTypes typ # QVars
- _nScheme :: Scheme (NomVarTypes typ) typ h
}
nParams :: forall typ h. Lens' (NominalDecl typ h) ((#) (NomVarTypes typ) QVars)
nScheme :: forall typ h h. Lens (NominalDecl typ h) (NominalDecl typ h) (Scheme (NomVarTypes typ) typ h) (Scheme (NomVarTypes typ) typ h)
data W_NominalDecl (typ :: HyperType) node where
- W_NominalDecl_typ :: W_NominalDecl typ typ
data NominalInst nomId varTypes h = NominalInst {
- _nId :: nomId
- _nArgs :: varTypes # QVarInstances (GetHyperType h)
}
nId :: forall nomId varTypes h nomId. Lens (NominalInst nomId varTypes h) (NominalInst nomId varTypes h) nomId nomId
nArgs :: forall nomId varTypes h varTypes h. Lens (NominalInst nomId varTypes h) (NominalInst nomId varTypes h) ((#) varTypes (QVarInstances (GetHyperType h))) ((#) varTypes (QVarInstances (GetHyperType h)))
data ToNom nomId term h = ToNom {
- _tnId :: nomId
- _tnVal :: h :# term
}
tnId :: forall nomId term h nomId. Lens (ToNom nomId term h) (ToNom nomId term h) nomId nomId
tnVal :: forall nomId term h term h. Lens (ToNom nomId term h) (ToNom nomId term h) ((:#) h term) ((:#) h term)
data W_ToNom (nomId :: Type) (term :: HyperType) node where
- W_ToNom_term :: W_ToNom nomId term term
newtype FromNom nomId (term :: HyperType) (h :: AHyperType) = FromNom nomId
_FromNom :: forall nomId term h nomId term h. Iso (FromNom nomId term h) (FromNom nomId term h) nomId nomId
class HasNominalInst nomId typ where
- nominalInst :: Prism' (typ # h) (NominalInst nomId (NomVarTypes typ) # h)
type family NomVarTypes (t :: HyperType) :: HyperType
class MonadNominals nomId typ m where
- getNominalDecl :: nomId -> m (LoadedNominalDecl typ # UVarOf m)
data LoadedNominalDecl typ v
loadNominalDecl :: forall m typ. (HTraversable (NomVarTypes typ), HNodesConstraint (NomVarTypes typ) (Unify m), HasScheme (NomVarTypes typ) m typ) => (Pure # NominalDecl typ) -> m (LoadedNominalDecl typ # UVarOf m)

Documentation

data NominalDecl typ h Source #

A declaration of a nominal type.

Constructors

NominalDecl
Fields _nParams :: NomVarTypes typ # QVars _nScheme :: Scheme (NomVarTypes typ) typ h

Instances

Instances details

HFoldable (NominalDecl typ) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hfoldMap :: Monoid a => (forall (n :: HyperType). HWitness (NominalDecl typ) n -> (p # n) -> a) -> (NominalDecl typ # p) -> a Source #
HFunctor (NominalDecl typ) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hmap :: (forall (n :: HyperType). HWitness (NominalDecl typ) n -> (p # n) -> q # n) -> (NominalDecl typ # p) -> NominalDecl typ # q Source #
HNodes (NominalDecl typ) Source #
Instance details Defined in Hyper.Syntax.Nominal Associated Types type HNodesConstraint (NominalDecl typ) c Source # type HWitnessType (NominalDecl typ) :: HyperType -> Type Source # Methods hLiftConstraint :: forall c (n :: HyperType) r. HNodesConstraint (NominalDecl typ) c => HWitness (NominalDecl typ) n -> Proxy c -> (c n => r) -> r Source #
HTraversable (NominalDecl typ) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hsequence :: forall f (p :: AHyperType -> Type). Applicative f => (NominalDecl typ # ContainedH f p) -> f (NominalDecl typ # p) Source #
Generic (NominalDecl typ h) Source #
Instance details Defined in Hyper.Syntax.Nominal Associated Types type Rep (NominalDecl typ h) :: Type -> Type # Methods from :: NominalDecl typ h -> Rep (NominalDecl typ h) x # to :: Rep (NominalDecl typ h) x -> NominalDecl typ h #
Constraints (NominalDecl typ h) Show => Show (NominalDecl typ h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods showsPrec :: Int -> NominalDecl typ h -> ShowS # show :: NominalDecl typ h -> String # showList :: [NominalDecl typ h] -> ShowS #
Constraints (NominalDecl typ h) Binary => Binary (NominalDecl typ h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods put :: NominalDecl typ h -> Put # get :: Get (NominalDecl typ h) # putList :: [NominalDecl typ h] -> Put #
Constraints (NominalDecl typ h) NFData => NFData (NominalDecl typ h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods rnf :: NominalDecl typ h -> () #
Constraints (NominalDecl typ h) Eq => Eq (NominalDecl typ h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods (==) :: NominalDecl typ h -> NominalDecl typ h -> Bool # (/=) :: NominalDecl typ h -> NominalDecl typ h -> Bool #
Constraints (NominalDecl typ h) Ord => Ord (NominalDecl typ h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods compare :: NominalDecl typ h -> NominalDecl typ h -> Ordering # (<) :: NominalDecl typ h -> NominalDecl typ h -> Bool # (<=) :: NominalDecl typ h -> NominalDecl typ h -> Bool # (>) :: NominalDecl typ h -> NominalDecl typ h -> Bool # (>=) :: NominalDecl typ h -> NominalDecl typ h -> Bool # max :: NominalDecl typ h -> NominalDecl typ h -> NominalDecl typ h # min :: NominalDecl typ h -> NominalDecl typ h -> NominalDecl typ h #
type HWitnessType (NominalDecl typ) Source #
Instance details Defined in Hyper.Syntax.Nominal type HWitnessType (NominalDecl typ) = W_NominalDecl typ
type HNodesConstraint (NominalDecl typ) constraint Source #
Instance details Defined in Hyper.Syntax.Nominal type HNodesConstraint (NominalDecl typ) constraint = constraint typ
type Rep (NominalDecl typ h) Source #
Instance details Defined in Hyper.Syntax.Nominal type Rep (NominalDecl typ h) = D1 ('MetaData "NominalDecl" "Hyper.Syntax.Nominal" "hypertypes-0.2.2-9g9pX7Hb2mGI4yyssTDpOd" 'False) (C1 ('MetaCons "NominalDecl" 'PrefixI 'True) (S1 ('MetaSel ('Just "_nParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NomVarTypes typ # QVars)) :*: S1 ('MetaSel ('Just "_nScheme") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Scheme (NomVarTypes typ) typ h))))

nParams :: forall typ h. Lens' (NominalDecl typ h) ((#) (NomVarTypes typ) QVars) Source #

nScheme :: forall typ h h. Lens (NominalDecl typ h) (NominalDecl typ h) (Scheme (NomVarTypes typ) typ h) (Scheme (NomVarTypes typ) typ h) Source #

data W_NominalDecl (typ :: HyperType) node where Source #

Constructors

W_NominalDecl_typ :: W_NominalDecl typ typ

data NominalInst nomId varTypes h Source #

An instantiation of a nominal type

Constructors

NominalInst
Fields _nId :: nomId _nArgs :: varTypes # QVarInstances (GetHyperType h)

Instances

Instances details

(HFunctor varTypes, HContext varTypes, HNodesConstraint varTypes OrdQVar) => HContext (NominalInst nomId varTypes) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hcontext :: forall (p :: HyperType). (NominalInst nomId varTypes # p) -> NominalInst nomId varTypes # (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p) Source #
HFoldable v => HFoldable (NominalInst n v) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hfoldMap :: Monoid a => (forall (n0 :: HyperType). HWitness (NominalInst n v) n0 -> (p # n0) -> a) -> (NominalInst n v # p) -> a Source #
HFunctor v => HFunctor (NominalInst n v) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hmap :: (forall (n0 :: HyperType). HWitness (NominalInst n v) n0 -> (p # n0) -> q # n0) -> (NominalInst n v # p) -> NominalInst n v # q Source #
HNodes v => HNodes (NominalInst n v) Source #
Instance details Defined in Hyper.Syntax.Nominal Associated Types type HNodesConstraint (NominalInst n v) c Source # type HWitnessType (NominalInst n v) :: HyperType -> Type Source # Methods hLiftConstraint :: forall c (n0 :: HyperType) r. HNodesConstraint (NominalInst n v) c => HWitness (NominalInst n v) n0 -> Proxy c -> (c n0 => r) -> r Source #
HTraversable v => HTraversable (NominalInst n v) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hsequence :: forall f (p :: AHyperType -> Type). Applicative f => (NominalInst n v # ContainedH f p) -> f (NominalInst n v # p) Source #
(Eq nomId, ZipMatch varTypes, HTraversable varTypes, HNodesConstraint varTypes ZipMatch, HNodesConstraint varTypes OrdQVar) => ZipMatch (NominalInst nomId varTypes) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods zipMatch :: forall (p :: HyperType) (q :: HyperType). (NominalInst nomId varTypes # p) -> (NominalInst nomId varTypes # q) -> Maybe (NominalInst nomId varTypes # (p :*: q)) Source #
Generic (NominalInst nomId varTypes h) Source #
Instance details Defined in Hyper.Syntax.Nominal Associated Types type Rep (NominalInst nomId varTypes h) :: Type -> Type # Methods from :: NominalInst nomId varTypes h -> Rep (NominalInst nomId varTypes h) x # to :: Rep (NominalInst nomId varTypes h) x -> NominalInst nomId varTypes h #
Constraints (NominalInst nomId varTypes h) Show => Show (NominalInst nomId varTypes h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods showsPrec :: Int -> NominalInst nomId varTypes h -> ShowS # show :: NominalInst nomId varTypes h -> String # showList :: [NominalInst nomId varTypes h] -> ShowS #
Constraints (NominalInst nomId varTypes h) Binary => Binary (NominalInst nomId varTypes h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods put :: NominalInst nomId varTypes h -> Put # get :: Get (NominalInst nomId varTypes h) # putList :: [NominalInst nomId varTypes h] -> Put #
Constraints (NominalInst nomId varTypes h) NFData => NFData (NominalInst nomId varTypes h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods rnf :: NominalInst nomId varTypes h -> () #
Constraints (NominalInst nomId varTypes h) Eq => Eq (NominalInst nomId varTypes h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods (==) :: NominalInst nomId varTypes h -> NominalInst nomId varTypes h -> Bool # (/=) :: NominalInst nomId varTypes h -> NominalInst nomId varTypes h -> Bool #
Constraints (NominalInst nomId varTypes h) Ord => Ord (NominalInst nomId varTypes h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods compare :: NominalInst nomId varTypes h -> NominalInst nomId varTypes h -> Ordering # (<) :: NominalInst nomId varTypes h -> NominalInst nomId varTypes h -> Bool # (<=) :: NominalInst nomId varTypes h -> NominalInst nomId varTypes h -> Bool # (>) :: NominalInst nomId varTypes h -> NominalInst nomId varTypes h -> Bool # (>=) :: NominalInst nomId varTypes h -> NominalInst nomId varTypes h -> Bool # max :: NominalInst nomId varTypes h -> NominalInst nomId varTypes h -> NominalInst nomId varTypes h # min :: NominalInst nomId varTypes h -> NominalInst nomId varTypes h -> NominalInst nomId varTypes h #
(Pretty nomId, HApply varTypes, HFoldable varTypes, HNodesConstraint varTypes (PrettyConstraints h)) => Pretty (NominalInst nomId varTypes h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods pPrintPrec :: PrettyLevel -> Rational -> NominalInst nomId varTypes h -> Doc # pPrint :: NominalInst nomId varTypes h -> Doc # pPrintList :: PrettyLevel -> [NominalInst nomId varTypes h] -> Doc #
type HWitnessType (NominalInst n v) Source #
Instance details Defined in Hyper.Syntax.Nominal type HWitnessType (NominalInst n v) = HWitnessType v
type HNodesConstraint (NominalInst n v) c Source #
Instance details Defined in Hyper.Syntax.Nominal type HNodesConstraint (NominalInst n v) c = HNodesConstraint v c
type Rep (NominalInst nomId varTypes h) Source #
Instance details Defined in Hyper.Syntax.Nominal type Rep (NominalInst nomId varTypes h) = D1 ('MetaData "NominalInst" "Hyper.Syntax.Nominal" "hypertypes-0.2.2-9g9pX7Hb2mGI4yyssTDpOd" 'False) (C1 ('MetaCons "NominalInst" 'PrefixI 'True) (S1 ('MetaSel ('Just "_nId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 nomId) :*: S1 ('MetaSel ('Just "_nArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (varTypes # QVarInstances (GetHyperType h)))))

nId :: forall nomId varTypes h nomId. Lens (NominalInst nomId varTypes h) (NominalInst nomId varTypes h) nomId nomId Source #

nArgs :: forall nomId varTypes h varTypes h. Lens (NominalInst nomId varTypes h) (NominalInst nomId varTypes h) ((#) varTypes (QVarInstances (GetHyperType h))) ((#) varTypes (QVarInstances (GetHyperType h))) Source #

data ToNom nomId term h Source #

Nominal data constructor.

Wrap content with a data constructor (analogues to a data constructor of a Haskell `newtype`'s).

Introduces the nominal's foralled type variables into the value's scope.

Constructors

ToNom
Fields _tnId :: nomId _tnVal :: h :# term

Instances

Instances details

(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 #
Semigroup nomId => HApply (ToNom nomId term) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hzip :: forall (p :: HyperType) (q :: HyperType). (ToNom nomId term # p) -> (ToNom nomId term # q) -> ToNom nomId term # (p :*: q) Source #
HContext (ToNom nomId term) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hcontext :: forall (p :: HyperType). (ToNom nomId term # p) -> ToNom nomId term # (HFunc p (Const (ToNom nomId term # p)) :*: p) Source #
HFoldable (ToNom nomId term) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hfoldMap :: Monoid a => (forall (n :: HyperType). HWitness (ToNom nomId term) n -> (p # n) -> a) -> (ToNom nomId term # p) -> a Source #
HFunctor (ToNom nomId term) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hmap :: (forall (n :: HyperType). HWitness (ToNom nomId term) n -> (p # n) -> q # n) -> (ToNom nomId term # p) -> ToNom nomId term # q Source #
HNodes (ToNom nomId term) Source #
Instance details Defined in Hyper.Syntax.Nominal Associated Types type HNodesConstraint (ToNom nomId term) c Source # type HWitnessType (ToNom nomId term) :: HyperType -> Type Source # Methods hLiftConstraint :: forall c (n :: HyperType) r. HNodesConstraint (ToNom nomId term) c => HWitness (ToNom nomId term) n -> Proxy c -> (c n => r) -> r Source #
Monoid nomId => HPointed (ToNom nomId term) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hpure :: (forall (n :: HyperType). HWitness (ToNom nomId term) n -> p # n) -> ToNom nomId term # p Source #
HTraversable (ToNom nomId term) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hsequence :: forall f (p :: AHyperType -> Type). Applicative f => (ToNom nomId term # ContainedH f p) -> f (ToNom nomId term # p) Source #
Eq nomId => ZipMatch (ToNom nomId term) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods zipMatch :: forall (p :: HyperType) (q :: HyperType). (ToNom nomId term # p) -> (ToNom nomId term # q) -> Maybe (ToNom nomId term # (p :*: q)) Source #
HMorph (ToNom nomId term0) (ToNom nomId term1) Source #
Instance details Defined in Hyper.Syntax.Nominal Associated Types type MorphConstraint (ToNom nomId term0) (ToNom nomId term1) c Source # data MorphWitness (ToNom nomId term0) (ToNom nomId term1) :: HyperType -> HyperType -> Type Source # Methods morphMap :: (forall (a :: HyperType) (b :: HyperType). MorphWitness (ToNom nomId term0) (ToNom nomId term1) a b -> (p # a) -> q # b) -> (ToNom nomId term0 # p) -> ToNom nomId term1 # q Source # morphLiftConstraint :: forall c (a :: HyperType) (b :: HyperType) r. MorphConstraint (ToNom nomId term0) (ToNom nomId term1) c => MorphWitness (ToNom nomId term0) (ToNom nomId term1) a b -> Proxy c -> (c a b => r) -> r Source #
Generic (ToNom nomId term h) Source #
Instance details Defined in Hyper.Syntax.Nominal Associated Types type Rep (ToNom nomId term h) :: Type -> Type # Methods from :: ToNom nomId term h -> Rep (ToNom nomId term h) x # to :: Rep (ToNom nomId term h) x -> ToNom nomId term h #
Constraints (ToNom nomId term h) Show => Show (ToNom nomId term h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods showsPrec :: Int -> ToNom nomId term h -> ShowS # show :: ToNom nomId term h -> String # showList :: [ToNom nomId term h] -> ShowS #
Constraints (ToNom nomId term h) Binary => Binary (ToNom nomId term h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods put :: ToNom nomId term h -> Put # get :: Get (ToNom nomId term h) # putList :: [ToNom nomId term h] -> Put #
Constraints (ToNom nomId term h) NFData => NFData (ToNom nomId term h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods rnf :: ToNom nomId term h -> () #
Constraints (ToNom nomId term h) Eq => Eq (ToNom nomId term h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods (==) :: ToNom nomId term h -> ToNom nomId term h -> Bool # (/=) :: ToNom nomId term h -> ToNom nomId term h -> Bool #
Constraints (ToNom nomId term h) Ord => Ord (ToNom nomId term h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods compare :: ToNom nomId term h -> ToNom nomId term h -> Ordering # (<) :: ToNom nomId term h -> ToNom nomId term h -> Bool # (<=) :: ToNom nomId term h -> ToNom nomId term h -> Bool # (>) :: ToNom nomId term h -> ToNom nomId term h -> Bool # (>=) :: ToNom nomId term h -> ToNom nomId term h -> Bool # max :: ToNom nomId term h -> ToNom nomId term h -> ToNom nomId term h # min :: ToNom nomId term h -> ToNom nomId term h -> ToNom nomId term h #
Constraints (ToNom nomId term h) Pretty => Pretty (ToNom nomId term h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods pPrintPrec :: PrettyLevel -> Rational -> ToNom nomId term h -> Doc # pPrint :: ToNom nomId term h -> Doc # pPrintList :: PrettyLevel -> [ToNom nomId term h] -> Doc #
type InferOf (ToNom n e) Source #
Instance details Defined in Hyper.Syntax.Nominal type InferOf (ToNom n e) = NominalInst n (NomVarTypes (TypeOf e))
type HWitnessType (ToNom nomId term) Source #
Instance details Defined in Hyper.Syntax.Nominal type HWitnessType (ToNom nomId term) = W_ToNom nomId term
type HNodesConstraint (ToNom nomId term) constraint Source #
Instance details Defined in Hyper.Syntax.Nominal type HNodesConstraint (ToNom nomId term) constraint = constraint term
data MorphWitness (ToNom nomId term0) (ToNom nomId term1) _ _1 Source #
Instance details Defined in Hyper.Syntax.Nominal data MorphWitness (ToNom nomId term0) (ToNom nomId term1) _ _1 where M_ToNom_term :: forall nomId (term0 :: HyperType) (term1 :: HyperType). MorphWitness (ToNom nomId term0) (ToNom nomId term1) term0 term1
type MorphConstraint (ToNom nomId term0) (ToNom nomId term1) constraint Source #
Instance details Defined in Hyper.Syntax.Nominal type MorphConstraint (ToNom nomId term0) (ToNom nomId term1) constraint = constraint term0 term1
type Rep (ToNom nomId term h) Source #
Instance details Defined in Hyper.Syntax.Nominal type Rep (ToNom nomId term h) = D1 ('MetaData "ToNom" "Hyper.Syntax.Nominal" "hypertypes-0.2.2-9g9pX7Hb2mGI4yyssTDpOd" 'False) (C1 ('MetaCons "ToNom" 'PrefixI 'True) (S1 ('MetaSel ('Just "_tnId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 nomId) :*: S1 ('MetaSel ('Just "_tnVal") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (h :# term))))

tnId :: forall nomId term h nomId. Lens (ToNom nomId term h) (ToNom nomId term h) nomId nomId Source #

tnVal :: forall nomId term h term h. Lens (ToNom nomId term h) (ToNom nomId term h) ((:#) h term) ((:#) h term) Source #

data W_ToNom (nomId :: Type) (term :: HyperType) node where Source #

Constructors

W_ToNom_term :: W_ToNom nomId term term

newtype FromNom nomId (term :: HyperType) (h :: AHyperType) Source #

Access the data in a nominally typed value.

Analogues to a getter of a Haskell `newtype`.

Constructors

FromNom nomId

Instances

Instances details

(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 #
Semigroup nomId => HApply (FromNom nomId term) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hzip :: forall (p :: HyperType) (q :: HyperType). (FromNom nomId term # p) -> (FromNom nomId term # q) -> FromNom nomId term # (p :*: q) Source #
HContext (FromNom nomId term) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hcontext :: forall (p :: HyperType). (FromNom nomId term # p) -> FromNom nomId term # (HFunc p (Const (FromNom nomId term # p)) :*: p) Source #
HFoldable (FromNom nomId term) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hfoldMap :: Monoid a => (forall (n :: HyperType). HWitness (FromNom nomId term) n -> (p # n) -> a) -> (FromNom nomId term # p) -> a Source #
HFunctor (FromNom nomId term) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hmap :: (forall (n :: HyperType). HWitness (FromNom nomId term) n -> (p # n) -> q # n) -> (FromNom nomId term # p) -> FromNom nomId term # q Source #
HNodes (FromNom nomId term) Source #
Instance details Defined in Hyper.Syntax.Nominal Associated Types type HNodesConstraint (FromNom nomId term) c Source # type HWitnessType (FromNom nomId term) :: HyperType -> Type Source # Methods hLiftConstraint :: forall c (n :: HyperType) r. HNodesConstraint (FromNom nomId term) c => HWitness (FromNom nomId term) n -> Proxy c -> (c n => r) -> r Source #
Monoid nomId => HPointed (FromNom nomId term) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hpure :: (forall (n :: HyperType). HWitness (FromNom nomId term) n -> p # n) -> FromNom nomId term # p Source #
HTraversable (FromNom nomId term) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hsequence :: forall f (p :: AHyperType -> Type). Applicative f => (FromNom nomId term # ContainedH f p) -> f (FromNom nomId term # p) Source #
Eq nomId => ZipMatch (FromNom nomId term) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods zipMatch :: forall (p :: HyperType) (q :: HyperType). (FromNom nomId term # p) -> (FromNom nomId term # q) -> Maybe (FromNom nomId term # (p :*: q)) Source #
Generic (FromNom nomId term h) Source #
Instance details Defined in Hyper.Syntax.Nominal Associated Types type Rep (FromNom nomId term h) :: Type -> Type # Methods from :: FromNom nomId term h -> Rep (FromNom nomId term h) x # to :: Rep (FromNom nomId term h) x -> FromNom nomId term h #
Show nomId => Show (FromNom nomId term h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods showsPrec :: Int -> FromNom nomId term h -> ShowS # show :: FromNom nomId term h -> String # showList :: [FromNom nomId term h] -> ShowS #
Binary nomId => Binary (FromNom nomId term h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods put :: FromNom nomId term h -> Put # get :: Get (FromNom nomId term h) # putList :: [FromNom nomId term h] -> Put #
NFData nomId => NFData (FromNom nomId term h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods rnf :: FromNom nomId term h -> () #
Eq nomId => Eq (FromNom nomId term h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods (==) :: FromNom nomId term h -> FromNom nomId term h -> Bool # (/=) :: FromNom nomId term h -> FromNom nomId term h -> Bool #
Ord nomId => Ord (FromNom nomId term h) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods compare :: FromNom nomId term h -> FromNom nomId term h -> Ordering # (<) :: FromNom nomId term h -> FromNom nomId term h -> Bool # (<=) :: FromNom nomId term h -> FromNom nomId term h -> Bool # (>) :: FromNom nomId term h -> FromNom nomId term h -> Bool # (>=) :: FromNom nomId term h -> FromNom nomId term h -> Bool # max :: FromNom nomId term h -> FromNom nomId term h -> FromNom nomId term h # min :: FromNom nomId term h -> FromNom nomId term h -> FromNom nomId term h #
type InferOf (FromNom _1 e) Source #
Instance details Defined in Hyper.Syntax.Nominal type InferOf (FromNom _1 e) = FuncType (TypeOf e)
type HWitnessType (FromNom nomId term) Source #
Instance details Defined in Hyper.Syntax.Nominal type HWitnessType (FromNom nomId term) = V1 :: HyperType -> Type
type HNodesConstraint (FromNom nomId term) constraint Source #
Instance details Defined in Hyper.Syntax.Nominal type HNodesConstraint (FromNom nomId term) constraint = ()
type Rep (FromNom nomId term h) Source #
Instance details Defined in Hyper.Syntax.Nominal type Rep (FromNom nomId term h) = D1 ('MetaData "FromNom" "Hyper.Syntax.Nominal" "hypertypes-0.2.2-9g9pX7Hb2mGI4yyssTDpOd" 'True) (C1 ('MetaCons "FromNom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 nomId)))

_FromNom :: forall nomId term h nomId term h. Iso (FromNom nomId term h) (FromNom nomId term h) nomId nomId Source #

class HasNominalInst nomId typ where Source #

Methods

nominalInst :: Prism' (typ # h) (NominalInst nomId (NomVarTypes typ) # h) Source #

type family NomVarTypes (t :: HyperType) :: HyperType Source #

class MonadNominals nomId typ m where Source #

Methods

getNominalDecl :: nomId -> m (LoadedNominalDecl typ # UVarOf m) Source #

data LoadedNominalDecl typ v Source #

A nominal declaration loaded into scope in an inference monad.

Instances

Instances details

(Recursively HFoldable typ, HFoldable (NomVarTypes typ)) => HFoldable (LoadedNominalDecl typ) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hfoldMap :: Monoid a => (forall (n :: HyperType). HWitness (LoadedNominalDecl typ) n -> (p # n) -> a) -> (LoadedNominalDecl typ # p) -> a Source #
(Recursively HFunctor typ, HFunctor (NomVarTypes typ)) => HFunctor (LoadedNominalDecl typ) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hmap :: (forall (n :: HyperType). HWitness (LoadedNominalDecl typ) n -> (p # n) -> q # n) -> (LoadedNominalDecl typ # p) -> LoadedNominalDecl typ # q Source #
(RNodes t, HNodes (NomVarTypes t)) => HNodes (LoadedNominalDecl t) Source #
Instance details Defined in Hyper.Syntax.Nominal Associated Types type HNodesConstraint (LoadedNominalDecl t) c Source # type HWitnessType (LoadedNominalDecl t) :: HyperType -> Type Source # Methods hLiftConstraint :: forall c (n :: HyperType) r. HNodesConstraint (LoadedNominalDecl t) c => HWitness (LoadedNominalDecl t) n -> Proxy c -> (c n => r) -> r Source #
(RTraversable typ, HTraversable (NomVarTypes typ)) => HTraversable (LoadedNominalDecl typ) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods hsequence :: forall f (p :: AHyperType -> Type). Applicative f => (LoadedNominalDecl typ # ContainedH f p) -> f (LoadedNominalDecl typ # p) Source #
Generic (LoadedNominalDecl typ v) Source #
Instance details Defined in Hyper.Syntax.Nominal Associated Types type Rep (LoadedNominalDecl typ v) :: Type -> Type # Methods from :: LoadedNominalDecl typ v -> Rep (LoadedNominalDecl typ v) x # to :: Rep (LoadedNominalDecl typ v) x -> LoadedNominalDecl typ v #
Constraints (LoadedNominalDecl typ v) Show => Show (LoadedNominalDecl typ v) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods showsPrec :: Int -> LoadedNominalDecl typ v -> ShowS # show :: LoadedNominalDecl typ v -> String # showList :: [LoadedNominalDecl typ v] -> ShowS #
Constraints (LoadedNominalDecl typ v) Binary => Binary (LoadedNominalDecl typ v) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods put :: LoadedNominalDecl typ v -> Put # get :: Get (LoadedNominalDecl typ v) # putList :: [LoadedNominalDecl typ v] -> Put #
Constraints (LoadedNominalDecl typ v) NFData => NFData (LoadedNominalDecl typ v) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods rnf :: LoadedNominalDecl typ v -> () #
Constraints (LoadedNominalDecl typ v) Eq => Eq (LoadedNominalDecl typ v) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods (==) :: LoadedNominalDecl typ v -> LoadedNominalDecl typ v -> Bool # (/=) :: LoadedNominalDecl typ v -> LoadedNominalDecl typ v -> Bool #
Constraints (LoadedNominalDecl typ v) Ord => Ord (LoadedNominalDecl typ v) Source #
Instance details Defined in Hyper.Syntax.Nominal Methods compare :: LoadedNominalDecl typ v -> LoadedNominalDecl typ v -> Ordering # (<) :: LoadedNominalDecl typ v -> LoadedNominalDecl typ v -> Bool # (<=) :: LoadedNominalDecl typ v -> LoadedNominalDecl typ v -> Bool # (>) :: LoadedNominalDecl typ v -> LoadedNominalDecl typ v -> Bool # (>=) :: LoadedNominalDecl typ v -> LoadedNominalDecl typ v -> Bool # max :: LoadedNominalDecl typ v -> LoadedNominalDecl typ v -> LoadedNominalDecl typ v # min :: LoadedNominalDecl typ v -> LoadedNominalDecl typ v -> LoadedNominalDecl typ v #
type HWitnessType (LoadedNominalDecl t) Source #
Instance details Defined in Hyper.Syntax.Nominal type HWitnessType (LoadedNominalDecl t)
type HNodesConstraint (LoadedNominalDecl t) c Source #
Instance details Defined in Hyper.Syntax.Nominal type HNodesConstraint (LoadedNominalDecl t) c = (HNodesConstraint (NomVarTypes t) c, c t, Recursive c)
type Rep (LoadedNominalDecl typ v) Source #
Instance details Defined in Hyper.Syntax.Nominal type Rep (LoadedNominalDecl typ v) = D1 ('MetaData "LoadedNominalDecl" "Hyper.Syntax.Nominal" "hypertypes-0.2.2-9g9pX7Hb2mGI4yyssTDpOd" 'False) (C1 ('MetaCons "LoadedNominalDecl" 'PrefixI 'True) (S1 ('MetaSel ('Just "lnParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NomVarTypes typ # QVarInstances (GetHyperType v))) :: (S1 ('MetaSel ('Just "lnForalls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NomVarTypes typ # QVarInstances (GetHyperType v))) :: S1 ('MetaSel ('Just "lnType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (GTerm (GetHyperType v) # typ)))))

loadNominalDecl :: forall m typ. (HTraversable (NomVarTypes typ), HNodesConstraint (NomVarTypes typ) (Unify m), HasScheme (NomVarTypes typ) m typ) => (Pure # NominalDecl typ) -> m (LoadedNominalDecl typ # UVarOf m) Source #