Changes between Version 17 and Version 18 of Language/Core


Ignore:
Timestamp:
Dec 28, 2011, 9:36:31 AM (8 years ago)
Author:
benl
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Language/Core

    v17 v18  
    2121 * Level 0: Witnesses, also known as "capabilities", or "proof terms". When a witness exists in the program, a certain property of the system is guaranteed to be true.
    2222 * Level 1: Specifications. In Haskell these are called "types", but we avoid using that word here because we overload it to mean "kinds" and "sorts" as well. Specs classify both computation and witness expressions. A specification of a computation gives an upper bound on what might happen at runtime. A specification of a witness describes what property is true when the witness exists in the program.
    23  * Level 2: Kinds. Kinds classify specifications.
    24  * Level 3: Sort. Sorts classify kinds.
     23 * Level 2: Kinds classify specifications.
     24 * Level 3: Sorts classify kinds.
    2525
    2626 * In contrast to a language such as Gallina(Coq) or Agda, we only have a finite number of universe levels, and the structure of the higher levels is simpler than the lower ones.
     
    4444Constructors can have textual or symbolic names. A textual constructor starts with an upper case letter, and can be followed by upper and lower case letters, digits, underscores and primes. Named constructors can optionally end with a hash.
    4545
     46 * The {{{CON}}} grammar is used for both type and data constructors. Witness constructors have their own grammar.
    4647 * Constructors that end with a hash are used for unboxed types.
    4748 * ddci-core also uses constructors with a hash to represent store locations ({{{L0#}}}) and region handles ({{{R0#}}}).
     
    6364 * The kind arrow {{{(~>)}}} takes any kind to any kind, for example, both {{{* ~> *}}} and {{{% ~>!}}} are well typed.
    6465 * The implication arrow {{{(=>)}}} can have two possible kinds, shown above.
     66 * The implication arrow classifies a witness abstraction, which is always pure and total. The application of a witness to a witness abstraction does not perform an effect, and corresponds to logical implication elimination (modus ponens).
    6567 * The function arrow classifies a computation abstraction, which might diverge or perform some other effect when it is applied.
    66  * The implication arrow classifies a witness abstraction, which is always pure and total. The application of a witness to a witness abstraction does not perform an effect, and corresponds to logical implication elimination (modus ponens).
    6768
    6869=== Primitive named constructors ===
    6970
    70 The following witness kind constructors are baked into the language, have specific types, and cannot be redefined.
     71The following witness type constructors are baked into the language, have specific types, and cannot be redefined.
    7172
    7273 ||=Name=||=Type=||=Description=||
    7374 ||{{{Pure}}}|| {{{! ~> @}}} || Purity of an effect. ||
    7475 ||{{{Empty}}}|| {{{$ ~> @}}} || Emptiness of a closure. ||
    75  ||{{{Global}}}|| {{{% ~> @}}} || Region is allocated in the global pool. ||
    76  ||{{{DeepGlobal}}}|| {{{* ~> @}}} || All material regions in some type are allocated in the global pool. ||
    77  ||{{{Const}}}|| {{{% ~> @}}} || Region is constant. ||
     76 ||{{{Global}}}|| {{{% ~> @}}} || Objects in global regions are allocated in the heap, instead of on local stacks. ||
     77 ||{{{DeepGlobal}}}|| {{{* ~> @}}} || All material regions in some type are global. ||
     78 ||{{{Const}}}|| {{{% ~> @}}} || Objects in constant regions cannot be destructively updated. ||
    7879 ||{{{DeepConst}}}|| {{{* ~> @}}} || All material regions in some type are constant. ||
    79  ||{{{Mutable}}}|| {{{% ~> @}}} || Region is mutable. ||
     80 ||{{{Mutable}}}|| {{{% ~> @}}} || Objects in mutable regions may be destructively updated. ||
    8081 ||{{{DeepMutable}}}|| {{{* ~> @}}} || All material regions in some type are mutable. ||
    81  ||{{{Lazy}}}|| {{{% ~> @}}} || Region may contain thunks. ||
     82 ||{{{Lazy}}}|| {{{% ~> @}}} || Lazy regions may contain thunks instead of manifest objects. ||
    8283 ||{{{HeadLazy}}}|| {{{* ~> @}}} || Head region in some type may contain thunks. ||
    83  ||{{{Direct}}}|| {{{% ~> @}}} || Region does not contain thunks. ||
     84 ||{{{Manifest}}}|| {{{% ~> @}}} || Manifest regions do not contain thunks. ||
    8485 ||{{{DistinctN}}}|| {{{% ~> % ~> ... ~> @}}} || (N >= 2). Regions are distinct, and non-overlapping. ||
    8586
     
    8788 * A closure is {{{Empty}}} when all its {{{Use}}} components are on regions that are {{{Global}}}
    8889 * A region cannot be {{{Const}}} and {{{Mutable}}} at the same time.
    89  * A region cannot be {{{Lazy}}} and {{{Direct}}} at the same time.
    90 
    91 [[br]]
    92 The following are computation type constructors, and classify the dynamic behaviour of the system.
     90 * A region cannot be {{{Lazy}}} and {{{Manifest}}} at the same time.
     91
     92[[br]]
     93The following are computation type constructors.
    9394 ||=Name=||=Type=||=Description=||
    9495 ||{{{Read}}}||{{{% -> !}}}||Read effect on some region||
     
    111112}}}
    112113
    113 These are used at binding positions in both types and expressions. The hat {{{(^)}}} adds  deDebruijn index to the stack. The underscore (_) is a non-binding binder, or alternatively, is sugar for a named variable that is not free in the body of the binding construct.
    114 
    115  * During type checking, evaluation and optimisation, named variables are rewritten to deBruijn indices to avoid variable capture.
     114These are used at binding positions in both types and expressions. The hat {{{(^)}}} binder adds a debruijn index to the stack. The underscore (_) is a non-binding binder, or alternatively, is sugar for a named variable that is not free in the body of the binding construct.
     115
     116 * During type checking, evaluation and optimisation, named variables can be rewritten to debruijn indices to avoid name capture.
    116117
    117118[[br]]
     
    141142A type can be a variable, constructor, universally quantified type, type application, parenthesised type, type sum or arrow type.
    142143
    143 A type sum can also be the least-upper-bound of two types, the least effect, or the least closure.
    144 
    145 An arrow type can be the kind arrow, implication, the pure and empty function, the effectful and closureful function.
     144A type sum can be the least-upper-bound of two types, the least effect, or the least closure.
     145
     146An arrow type can be the kind arrow, implication, the pure and empty function, or the effectful and closureful function.
    146147
    147148 * The components of a type sum must have effect or closure kind.
    148149 * The kind arrow and implication arrows must be fully applied.
    149  * With the function arrow, the first and last type arguments are the parameter and return types. The second and third type arguments are the effect and closure of the function.
     150 * With the function arrow, the first and last arguments are the parameter and return types. The second and third arguments are the effect and closure of the function.
    150151
    151152The following type expressions are equivalent:
     
    202203ARGWITS  ::= < WIT  >  | <: ARGWIT+  :>
    203204
    204 ARGTYPE  ::= VAR | CON | !0 | $0 | (TYPE)
    205 ARGWIT   ::= VAR | CON | (WITNESS)
     205ARGTYPE  ::= VAR | CON | !0 | $0 | ( TYPE )
     206ARGWIT   ::= VAR | CON | ( WITNESS )
    206207}}}
    207208
     
    223224 ||U||{{{alloc}}}||{{{[r:%].Const r => Pure (Alloc r)}}}||
    224225
    225  * Runtime witness constructors are marked with (R), and are introduced into the program at runtime. They cannot appear in the source code. They are introduced by the system only when the associated property is true, and the type system ensures that they are eliminated from the program when this is no longer the case.
    226  * User witness constructors are marked with (U), and can be used in the source program. The user witness constructors are either always true, as with the axioms {{{pure}}} and {{{empty}}}, or combine existing witnesses, as with {{{use}}}, {{{read}}} and {{{alloc}}}.
     226 * Runtime witness constructors are marked with (R). These are introduced into the program at runtime and cannot appear in the source code. They are introduced by the system only when the associated property is true, and the type system ensures that they are eliminated from the program when this is no longer the case.
     227 * User witness constructors are marked with (U). These can be used in the source code. The user witness constructors are either always true, as with the axioms {{{pure}}} and {{{empty}}}, or combine existing witnesses in a sound way, as with {{{use}}}, {{{read}}} and {{{alloc}}}.
    227228
    228229 * Only witnesses of types {{{Pure t}}} or {{{Empty t}}} can be joined, for some type {{{t}}}.