Safe Haskell | Safe-Infered |
---|
Abstract syntax for the Disciple core language.
- module DDC.Type.Exp
- data Exp a n
- data Cast n
- = CastWeakenEffect (Effect n)
- | CastWeakenClosure (Closure n)
- | CastPurify (Witness n)
- | CastForget (Witness n)
- data Lets a n
- data LetMode n
- data Alt a n = AAlt (Pat n) (Exp a n)
- data Pat n
- data Witness n
- data WiCon n
- = WiConBuiltin WbCon
- | WiConBound (Bound n)
- data WbCon
- = WbConPure
- | WbConEmpty
- | WbConUse
- | WbConRead
- | WbConAlloc
Documentation
module DDC.Type.Exp
Computation expressions
Well-typed expressions live in the Data universe, and their types always
have kind *
.
Expressions do something useful at runtime, and might diverge or cause side effects.
XVar a (Bound n) | Value variable or primitive operation. |
XCon a (Bound n) | Data constructor or literal. |
XLAM a (Bind n) (Exp a n) | Type abstraction (level-1). |
XLam a (Bind n) (Exp a n) | Value and Witness abstraction (level-0). |
XApp a (Exp a n) (Exp a n) | Application. |
XLet a (Lets a n) (Exp a n) | Possibly recursive bindings. |
XCase a (Exp a n) [Alt a n] | Case branching. |
XCast a (Cast n) (Exp a n) | Type cast. |
XType (Type n) | Type can appear as the argument of an application. |
XWitness (Witness n) | Witness can appear as the argument of an application. |
Type casts.
CastWeakenEffect (Effect n) | Weaken the effect of an expression. |
CastWeakenClosure (Closure n) | Weaken the closure of an expression. |
CastPurify (Witness n) | Purify the effect of an expression. |
CastForget (Witness n) | Hide sharing of the closure of an expression. |
Possibly recursive bindings.
Describes how a let binding should be evaluated.
Case alternatives.
Pattern matching.
Witnesses expressions
When a witness exists in the program it guarantees that a certain property of the program is true.
Witness constructors.
WiConBuiltin WbCon | Witness constructors baked into the language. |
WiConBound (Bound n) | Witness constructors defined in the environment. In the interpreter we use this to hold runtime capabilities. |
Built-in witness constructors.
These are used to convert a runtime capability into a witness that the corresponding property is true.
WbConPure | (axiom) The pure effect is pure. pure :: Pure !0 |
WbConEmpty | (axiom) The empty closure is empty. empty :: Empty $0 |
WbConUse | Convert a capability guaranteeing that a region is in the global heap into a witness that a closure using this region is empty. This lets us rely on the garbage collector to reclaim objects in the region. It is needed when we suspend the evaluation of expressions that have a region in their closure, because the type of the returned thunk may not reveal that it references objects in that region. use :: [r: %]. Global r => Empty (Use r) |
WbConRead | Convert a capability guaranteeing the constancy of a region into a witness that a read from that region is pure. This lets us suspend applications that read constant objects, because it doesn't matter if the read is delayed, we'll always get the same result. read :: [r: %]. Const r => Pure (Read r) |
WbConAlloc | Convert a capability guaranteeing the constancy of a region into a witness that allocation into that region is pure. This lets us increase the sharing of constant objects, because we can't tell constant objects of the same value apart. alloc :: [r: %]. Const r => Pure (Alloc r) |