Disciple Core Language

Disciple Core is an explicitly typed languages based on System-F2, intended as an intermediate representation for a compiler. In addition to the features of System-F2 it supports region, effect and closure typing. Evaluation order is left-to-right call-by-value by default, but explicit lazy evaluation is also supported. There is also a capability system to track whether objects are mutable or constant, and to ensure that computations that perform visible side effects are not suspended with lazy evaluation.

Disciple Core

• Universes
• Variables and Constructors
• Types
• Witnesses
• Expressions
• Modules

Flavours

DDC uses several separate flavours of the core language. Each flavour consists of a fragment of the full Disciple Core language, along with a set of primitive types and operators specific to the flavour.

• Disciple Core Lite
• Disciple Core Salt
• Disciple Core Eval