Wit     ::= Var
         |  WitCon
         |  Wit WitArg
         |  Wit '&' Wit

WitArg  ::= Wit | [ Type ]

A witness can be a variable, witness constructor, application or witness join.

Only witnesses of types Purify t or Emptify t can be joined, for some type t.

Witness Constructors

These following witness constructors encode axioms and rules in the type system. They are always valid and be used directly in the core program.

pure Purify Pure
empty Emptify Empty
use [r : Region].Global r => Emptify (Use r)
read [r : Region].Const r => Purify (Read r)
alloc [r : Region].Const r => Purify (Alloc r)

These following witness constructors represent runtime capabilities. Obstinately they are only created at runtime, but for testing purposes we also inject them into the code programs accepted by the interpreter. The type system ensures that the capability can only be present in the program when the corresponding property is true.

Global# [r : Region].Global r
Const# [r : Region].Const r
Mutable# [r : Region].Mutable r
Lazy# [r : Region].Lazy r
Direct# [r : Region].Direct r

Sugar and Equivalences

The following witness expressions are equivalent:

(Wit) = WIT
Wit1 Wit2 Wit3 = (Wit1 Wit2) Wit3
Wit [:AType1 AType2 ... ATypeN:] = Wit [AType1] [AType2] ... [ATypeN] Note A
Wit1 & Wit2 = Wit2 & Wit1
(Wit1 & Wit2) & Wit3 = Wit1 & (Wit2 & Wit3)

Note A: In the type application sugar, the types used in the list must have the following syntax. This ensures there is no ambiguity between successive arguments.



 1) pure  :: Pure !0

 2) Const# [r1] :: Const r1

 3) read [r1] w1 :: Pure (Read r1) 
    ... where w1 :: Const r1

 4) read [r1] w1 & alloc [r2] w2 :: Pure (Read r1 + Alloc r1)
    ... where w1 :: Const r1  and  w2 :: Const r2


  • 2013/8: Changed <: ... :> sugar to use braces to reclaim the angle bracket token for comparison operators.
  • 2011/12: Split the Witness universe from the Spec universe.
  • 2011/12: Added multiple application sugar {: ... :} and <: ... :> to beautify the core programs. This helps with recursive functions when many type variables need to be passed back in the recursive call.
  • 2009: Introduced a polymorphic witness join operator (&) instead of using join constructors MkJoinEffect and MkJoinClosure. These cluttered the core programs too much.
Last modified 3 years ago Last modified on Mar 8, 2014, 5:52:51 AM