AST.Knot.Pure

A Knot to express the simplest plain form of a nested higher-kinded data structure.

The value level hyperfunctions equivalent of Pure is called self in Hyperfunctions papers.

Documentation

newtype Pure k

A Knot to express the simplest plain form of a nested higher-kinded data structure

Constructors

Pure (k # Pure)

Instances

KNodes Pure

Defined in AST.Knot.Pure

Associated Types

type KNodesConstraint Pure c :: Constraint

data KWitness Pure a :: Type

Methods

kLiftConstraint :: KNodesConstraint Pure c => KWitness Pure n -> Proxy c -> (c n -> r) -> r

KPointed Pure

Defined in AST.Knot.Pure

Methods

pureK :: (forall (n :: Knot -> Type). KWitness Pure n -> Tree p n) -> Tree Pure p

KFunctor Pure

Defined in AST.Knot.Pure

Methods

mapK :: (forall (n :: Knot -> Type). KWitness Pure n -> Tree p n -> Tree q n) -> Tree Pure p -> Tree Pure q

KApply Pure

Defined in AST.Knot.Pure

Methods

zipK :: Tree Pure p -> Tree Pure q -> Tree Pure (Product p q)

KFoldable Pure

Defined in AST.Knot.Pure

Methods

foldMapK :: Monoid a => (forall (n :: Knot -> Type). KWitness Pure n -> Tree p n -> a) -> Tree Pure p -> a

KTraversable Pure

Defined in AST.Knot.Pure

Methods

sequenceK :: Applicative f => Tree Pure (ContainedK f p) -> f (Tree Pure p)

ZipMatch Pure

Defined in AST.Class.ZipMatch

Methods

zipMatch :: Tree Pure p -> Tree Pure q -> Maybe (Tree Pure (Product p q))

RTraversable Pure

Defined in AST.Class.Recursive

Methods

recursiveKTraversable :: Proxy Pure -> Dict (KNodesConstraint Pure RTraversable)

RNodes Pure

Defined in AST.Class.Recursive

Methods

recursiveKNodes :: Proxy Pure -> Dict (KNodesConstraint Pure RNodes)

KMonad Pure

Defined in AST.Class.Monad

Methods

joinK :: Recursively KFunctor p => Tree (Compose Pure Pure) p -> Tree Pure p

c Pure => Recursively c Pure

Defined in AST.Class.Recursive

Methods

recursively :: Proxy (c Pure) -> Dict (c Pure, KNodesConstraint Pure (Recursively c))

Constraints (Pure k) Eq => Eq (Pure k)

Defined in AST.Knot.Pure

Methods

(==) :: Pure k -> Pure k -> Bool

(/=) :: Pure k -> Pure k -> Bool

Constraints (Pure k) Ord => Ord (Pure k)

Defined in AST.Knot.Pure

Methods

compare :: Pure k -> Pure k -> Ordering

(<) :: Pure k -> Pure k -> Bool

(<=) :: Pure k -> Pure k -> Bool

(>) :: Pure k -> Pure k -> Bool

(>=) :: Pure k -> Pure k -> Bool

max :: Pure k -> Pure k -> Pure k

min :: Pure k -> Pure k -> Pure k

Constraints (Pure k) Show => Show (Pure k)

Defined in AST.Knot.Pure

Methods

showsPrec :: Int -> Pure k -> ShowS

show :: Pure k -> String

showList :: [Pure k] -> ShowS

Generic (Pure k)

Defined in AST.Knot.Pure

Associated Types

type Rep (Pure k) :: Type -> Type

Methods

from :: Pure k -> Rep (Pure k) x

to :: Rep (Pure k) x -> Pure k

Constraints (Pure k) Binary => Binary (Pure k)

Defined in AST.Knot.Pure

Methods

put :: Pure k -> Put

get :: Get (Pure k)

putList :: [Pure k] -> Put

Constraints (Pure k) NFData => NFData (Pure k)

Defined in AST.Knot.Pure

Methods

rnf :: Pure k -> ()

Pretty (k # Pure) => Pretty (Pure k)

Defined in AST.Knot.Pure

Methods

pPrintPrec :: PrettyLevel -> Rational -> Pure k -> Doc

pPrint :: Pure k -> Doc

pPrintList :: PrettyLevel -> [Pure k] -> Doc

data KWitness Pure node

Defined in AST.Knot.Pure

data KWitness Pure node where

• W_Pure_Pure :: forall (node :: Knot -> Type). KWitness Pure Pure

type KNodesConstraint Pure constraint

Defined in AST.Knot.Pure

type KNodesConstraint Pure constraint = constraint Pure

type Rep (Pure k)

Defined in AST.Knot.Pure

type Rep (Pure k) = D1 (MetaData "Pure" "AST.Knot.Pure" "syntax-tree-0.1.0.0-8tfou50n4eQ4Iq1dis9DWN" True) (C1 (MetaCons "Pure" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (k # Pure))))

_Pure :: Iso (Tree Pure k) (Tree Pure j) (Tree k Pure) (Tree j Pure)

An Iso from Pure to its content.

Using _Pure rather than the Pure data constructor is recommended, because it helps the type inference know that Pure is parameterized with a Knot.

data family KWitness k :: (Knot -> Type) -> Type

KWitness k n is a witness that n is a node of k

Instances

data KWitness Pure node

Defined in AST.Knot.Pure

data KWitness Pure node where

• W_Pure_Pure :: forall (node :: Knot -> Type). KWitness Pure Pure

data KWitness Prune node

Defined in AST.Knot.Prune

data KWitness Prune node where

• W_Prune_Prune :: forall (node :: Knot -> Type). KWitness Prune Prune

data KWitness (ANode c) node

Defined in AST.Combinator.ANode

data KWitness (ANode c) node where

• W_ANode_c :: forall (c :: Knot -> Type) (node :: Knot -> Type). KWitness (ANode c) c

data KWitness (F f) node

Defined in AST.Knot.Functor

data KWitness (F f) node where

• W_F_F_f :: forall (f :: Type -> Type) (node :: Knot -> Type). KWitness (F f) (F f)

data KWitness (Ann a) node

Defined in AST.Knot.Ann

data KWitness (Ann a) node where

• W_Ann_Ann_a :: forall a (node :: Knot -> Type). KWitness (Ann a) (Ann a)

data KWitness (UnifyError t) n

Defined in AST.Unify.Error

data KWitness (UnifyError t) n where

• W_UnifyError_t :: forall (t :: Knot -> Type) (n :: Knot -> Type). KWitness (UnifyError t) t
• E_UnifyError_t :: forall (t :: Knot -> Type) (n :: Knot -> Type). KWitness t n -> KWitness (UnifyError t) n

data KWitness (FuncType typ) node

Defined in AST.Term.FuncType

data KWitness (FuncType typ) node where

• W_FuncType_typ :: forall (typ :: Knot -> Type) (node :: Knot -> Type). KWitness (FuncType typ) typ

data KWitness (LoadedNominalDecl t) n

Defined in AST.Term.Nominal

data KWitness (LoadedNominalDecl t) n

• = E_LoadedNominalDecl_Body (KRecWitness t n)
• | E_LoadedNominalDecl_NomVarTypes (KWitness (NomVarTypes t) n)

data KWitness (NominalDecl typ) node

Defined in AST.Term.Nominal

data KWitness (NominalDecl typ) node = E_NominalDecl_Scheme_NomVarTypes_typ_typ (KWitness (Scheme (NomVarTypes typ) typ) node)

data KWitness (App expr) node

Defined in AST.Term.App

data KWitness (App expr) node where

• W_App_expr :: forall (expr :: Knot -> Type) (node :: Knot -> Type). KWitness (App expr) expr

data KWitness (ScopeTypes t) node

Defined in AST.Term.NamelessScope

data KWitness (ScopeTypes t) node where

• W_ScopeTypes_t :: forall (t :: Knot -> Type) (node :: Knot -> Type). KWitness (ScopeTypes t) t

data KWitness (Const a :: Knot -> Type) i

Defined in AST.Class.Nodes

data KWitness (Const a :: Knot -> Type) i

data KWitness (Flip GTerm a) n

Defined in AST.Unify.Generalize

data KWitness (Flip GTerm a) n = E_Flip_GTerm (KRecWitness a n)

data KWitness (Flip (ITerm a) e) n

Defined in AST.Infer.Term

data KWitness (Flip (ITerm a) e) n where

• E_Flip_ITerm_InferOf_e :: forall a (e :: Knot -> Type) (n :: Knot -> Type). KWitness (InferOf e) n -> KWitness (Flip (ITerm a) e) n
• E_Flip_ITerm_e :: forall a (e :: Knot -> Type) (n :: Knot -> Type) (f :: Knot -> Type). KWitness e f -> KWitness (Flip (ITerm a) f) n -> KWitness (Flip (ITerm a) e) n

data KWitness (Flip (BTerm a) e) n

Defined in AST.Infer.Blame

data KWitness (Flip (BTerm a) e) n where

• E_Flip_BTerm_InferOf_e :: forall a (e :: Knot -> Type) (n :: Knot -> Type). KWitness (InferOf e) n -> KWitness (Flip (BTerm a) e) n
• E_Flip_BTerm_e :: forall a (e :: Knot -> Type) (n :: Knot -> Type) (f :: Knot -> Type). KWitness e f -> KWitness (Flip (BTerm a) f) n -> KWitness (Flip (BTerm a) e) n

data KWitness (Compose a b) n

Defined in AST.Combinator.Compose

data KWitness (Compose a b) n where

• KWitness_Compose :: forall (a :: Knot -> Type) (b :: Knot -> Type) (n :: Knot -> Type) (a0 :: Knot -> Type) (b0 :: Knot -> Type). KWitness a a0 -> KWitness b b0 -> KWitness (Compose a b) (Compose a0 b0)

data KWitness (TermMap k expr) node

Defined in AST.Term.Map

data KWitness (TermMap k expr) node where

• W_TermMap_expr :: forall k (expr :: Knot -> Type) (node :: Knot -> Type). KWitness (TermMap k expr) expr

data KWitness (Var v expr) node

Defined in AST.Term.Var

data KWitness (Var v expr) node

data KWitness (Scheme varTypes typ) node

Defined in AST.Term.Scheme

data KWitness (Scheme varTypes typ) node where

• W_Scheme_typ :: forall (varTypes :: Knot -> Type) (typ :: Knot -> Type) (node :: Knot -> Type). KWitness (Scheme varTypes typ) typ

data KWitness (TypeSig vars term) node

Defined in AST.Term.TypeSig

data KWitness (TypeSig vars term) node where

• W_TypeSig_term :: forall (vars :: Knot -> Type) (term :: Knot -> Type) (node :: Knot -> Type). KWitness (TypeSig vars term) term
• W_TypeSig_Scheme_vars_TypeOf_term :: forall (vars :: Knot -> Type) (term :: Knot -> Type) (node :: Knot -> Type). KWitness (TypeSig vars term) (Scheme vars (TypeOf term))

data KWitness (FromNom nomId term) node

Defined in AST.Term.Nominal

data KWitness (FromNom nomId term) node

data KWitness (ToNom nomId term) node

Defined in AST.Term.Nominal

data KWitness (ToNom nomId term) node where

• W_ToNom_term :: forall nomId (term :: Knot -> Type) (node :: Knot -> Type). KWitness (ToNom nomId term) term

data KWitness (NominalInst n v) c

Defined in AST.Term.Nominal

data KWitness (NominalInst n v) c = E_NominalInst_k (KWitness v c)

data KWitness (Let v expr) node

Defined in AST.Term.Let

data KWitness (Let v expr) node where

• W_Let_expr :: forall v (expr :: Knot -> Type) (node :: Knot -> Type). KWitness (Let v expr) expr

data KWitness (Lam v expr) node

Defined in AST.Term.Lam

data KWitness (Lam v expr) node where

• W_Lam_expr :: forall v (expr :: Knot -> Type) (node :: Knot -> Type). KWitness (Lam v expr) expr

data KWitness (Scope expr a) node

Defined in AST.Term.NamelessScope

data KWitness (Scope expr a) node where

• W_Scope_expr_Maybe_a :: forall (expr :: Type -> Knot -> Type) a (node :: Knot -> Type). KWitness (Scope expr a) (expr (Maybe a))

data KWitness (ScopeVar expr a) node

Defined in AST.Term.NamelessScope

data KWitness (ScopeVar expr a) node

data KWitness (Product a b) n

Defined in AST.Class.Nodes

data KWitness (Product a b) n

• = E_Product_a (KWitness a n)
• | E_Product_b (KWitness b n)

data KWitness (Sum a b) n

Defined in AST.Class.Nodes

data KWitness (Sum a b) n

• = E_Sum_a (KWitness a n)
• | E_Sum_b (KWitness b n)

data KWitness (FlatRowExtends key val rest) node

Defined in AST.Term.Row

data KWitness (FlatRowExtends key val rest) node where

• W_FlatRowExtends_val :: forall key (val :: Knot -> Type) (rest :: Knot -> Type) (node :: Knot -> Type). KWitness (FlatRowExtends key val rest) val
• W_FlatRowExtends_rest :: forall key (val :: Knot -> Type) (rest :: Knot -> Type) (node :: Knot -> Type). KWitness (FlatRowExtends key val rest) rest

data KWitness (RowExtend key val rest) node

Defined in AST.Term.Row

data KWitness (RowExtend key val rest) node where

• W_RowExtend_val :: forall key (val :: Knot -> Type) (rest :: Knot -> Type) (node :: Knot -> Type). KWitness (RowExtend key val rest) val
• W_RowExtend_rest :: forall key (val :: Knot -> Type) (rest :: Knot -> Type) (node :: Knot -> Type). KWitness (RowExtend key val rest) rest

data KWitness (TypedLam var typ expr) node

Defined in AST.Term.TypedLam

data KWitness (TypedLam var typ expr) node where

• W_TypedLam_typ :: forall var (typ :: Knot -> Type) (expr :: Knot -> Type) (node :: Knot -> Type). KWitness (TypedLam var typ expr) typ
• W_TypedLam_expr :: forall var (typ :: Knot -> Type) (expr :: Knot -> Type) (node :: Knot -> Type). KWitness (TypedLam var typ expr) expr

(&#) :: a -> (a -> Tree k Pure) -> Tree Pure k infixl 1

An operator to apply a function to a value and wrap it with Pure.

Helps value construction be more succinct.

The etymology and fixity of &# operator mimics &.

>>> x &# f
Pure (f x)