AST.Term.FuncType

Documentation

data FuncType typ k

A term for the types of functions. Analogues to (->) in Haskell.

FuncType typs express types of functions of typ.

The data type comes along with the HasFuncType class for code to be able to work for any type AST supporting the types of functions.

Constructors

FuncType

Fields

• _funcIn :: k # typ
• _funcOut :: k # typ

Instances

KNodes (FuncType typ)

Defined in AST.Term.FuncType

Associated Types

type KNodesConstraint (FuncType typ) c :: Constraint

data KWitness (FuncType typ) a :: Type

Methods

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

KPointed (FuncType typ)

Defined in AST.Term.FuncType

Methods

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

KFunctor (FuncType typ)

Defined in AST.Term.FuncType

Methods

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

KApply (FuncType typ)

Defined in AST.Term.FuncType

Methods

zipK :: Tree (FuncType typ) p -> Tree (FuncType typ) q -> Tree (FuncType typ) (Product p q)

KFoldable (FuncType typ)

Defined in AST.Term.FuncType

Methods

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

KTraversable (FuncType typ)

Defined in AST.Term.FuncType

Methods

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

ZipMatch (FuncType typ)

Defined in AST.Term.FuncType

Methods

zipMatch :: Tree (FuncType typ) p -> Tree (FuncType typ) q -> Maybe (Tree (FuncType typ) (Product p q))

Constraints (FuncType typ k) Eq => Eq (FuncType typ k)

Defined in AST.Term.FuncType

Methods

(==) :: FuncType typ k -> FuncType typ k -> Bool

(/=) :: FuncType typ k -> FuncType typ k -> Bool

Constraints (FuncType typ k) Ord => Ord (FuncType typ k)

Defined in AST.Term.FuncType

Methods

compare :: FuncType typ k -> FuncType typ k -> Ordering

(<) :: FuncType typ k -> FuncType typ k -> Bool

(<=) :: FuncType typ k -> FuncType typ k -> Bool

(>) :: FuncType typ k -> FuncType typ k -> Bool

(>=) :: FuncType typ k -> FuncType typ k -> Bool

max :: FuncType typ k -> FuncType typ k -> FuncType typ k

min :: FuncType typ k -> FuncType typ k -> FuncType typ k

Show (k # typ) => Show (FuncType typ k)

Defined in AST.Term.FuncType

Methods

showsPrec :: Int -> FuncType typ k -> ShowS

show :: FuncType typ k -> String

showList :: [FuncType typ k] -> ShowS

Generic (FuncType typ k)

Defined in AST.Term.FuncType

Associated Types

type Rep (FuncType typ k) :: Type -> Type

Methods

from :: FuncType typ k -> Rep (FuncType typ k) x

to :: Rep (FuncType typ k) x -> FuncType typ k

Constraints (FuncType typ k) Binary => Binary (FuncType typ k)

Defined in AST.Term.FuncType

Methods

put :: FuncType typ k -> Put

get :: Get (FuncType typ k)

putList :: [FuncType typ k] -> Put

Constraints (FuncType typ k) NFData => NFData (FuncType typ k)

Defined in AST.Term.FuncType

Methods

rnf :: FuncType typ k -> ()

Pretty (k # typ) => Pretty (FuncType typ k)

Defined in AST.Term.FuncType

Methods

pPrintPrec :: PrettyLevel -> Rational -> FuncType typ k -> Doc

pPrint :: FuncType typ k -> Doc

pPrintList :: PrettyLevel -> [FuncType typ k] -> Doc

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

type KNodesConstraint (FuncType typ) constraint

Defined in AST.Term.FuncType

type KNodesConstraint (FuncType typ) constraint = constraint typ

type Rep (FuncType typ k)

Defined in AST.Term.FuncType

type Rep (FuncType typ k) = D1 (MetaData "FuncType" "AST.Term.FuncType" "syntax-tree-0.1.0.0-8tfou50n4eQ4Iq1dis9DWN" False) (C1 (MetaCons "FuncType" PrefixI True) (S1 (MetaSel (Just "_funcIn") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (k # typ)) :*: S1 (MetaSel (Just "_funcOut") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (k # typ))))

funcIn :: forall typ k. Lens' (FuncType typ k) ((#) k typ)

funcOut :: forall typ k. Lens' (FuncType typ k) ((#) k typ)

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

class HasFuncType typ where

HasFuncType is a class of Knots representing types that support the types of functions.

It is used by the Infer instances of App and Lam to work for any AST which provides HasFuncType.

Methods

funcType :: Prism' (Tree typ k) (Tree (FuncType typ) k)