Safe Haskell | Safe |
---|---|
Language | Haskell98 |
- module DDC.Type.Exp
- data Exp a n
- data Cast a n
- = CastWeakenEffect !(Effect n)
- | CastPurify !(Witness a n)
- | CastBox
- | CastRun
- data Lets a n
- data Alt a n = AAlt !(Pat n) !(Exp a n)
- data Pat n
- data Witness a n
- data DaCon n t :: * -> * -> *
- data WiCon n :: * -> * = WiConBound ~(Bound n) ~(Type n)
- type KindEnvF = Env Name
- type TypeEnvF = Env Name
- type TypeF = Type Name
- type ModuleF = Module () Name
- type ExpF = Exp () Name
- type CastF = Cast () Name
- type LetsF = Lets () Name
- type AltF = Alt () Name
- type PatF = Pat Name
- type WitnessF = Witness () Name
- type BoundF = Bound Name
- type BindF = Bind Name
Documentation
module DDC.Type.Exp
Expressions
Well-typed expressions have types of kind Data
.
XAnnot a (Exp a n) | Annotation. |
XVar !(Bound n) | Value variable or primitive operation. |
XCon !(DaCon n (Type n)) | Data constructor or literal. |
XLAM !(Bind n) !(Exp a n) | Type abstraction (level-1). |
XLam !(Bind n) !(Exp a n) | Value and Witness abstraction (level-0). |
XApp !(Exp a n) !(Exp a n) | Application. |
XLet !(Lets a n) !(Exp a n) | Possibly recursive bindings. |
XCase !(Exp a n) ![Alt a n] | Case branching. |
XCast !(Cast a n) !(Exp a n) | Type cast. |
XType !(Type n) | Type can appear as the argument of an application. |
XWitness !(Witness a n) | Witness can appear as the argument of an application. |
Type casts.
CastWeakenEffect !(Effect n) | Weaken the effect of an expression. The given effect is added to the effect of the body. |
CastPurify !(Witness a n) | Purify the effect (action) of an expression. |
CastBox | Box up a computation, capturing its effects in the S computation type. |
CastRun | Run a computation, releasing its effects into the environment. |
Possibly recursive bindings.
Case alternatives.
Pattern matching.
Witnesses
When a witness exists in the program it guarantees that a certain property of the program is true.
Data Constructors
data DaCon n t :: * -> * -> * #
Data constructors.
DaConUnit | Baked in unit data constructor. |
DaConPrim | Primitive data constructor used for literals and baked-in constructors. The type of the constructor needs to be attached to handle the case where there are too many constructors in the data type to list, like for Int literals. In this case we determine what data type it belongs to from the attached type of the data constructor. |
DaConBound | Data constructor that has a data type declaration. |
|
Witness Constructors
Witness constructors.
WiConBound ~(Bound n) ~(Type n) | Witness constructors defined in the environment. In the interpreter we use this to hold runtime capabilities. The attached type must be closed. |