wiki:Language/Core/Witnesses

Version 14 (modified by benl, 8 years ago) (diff)

Remove unimplemented distinct constructor

Witnesses

WIT  ::= VAR
      |  WCON
      |  WIT WARG
      |  WIT & WIT

WARG ::= WIT | [ TYPE ]

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

Witness Constructors

All the witness constructors are baked in, and are listed below.

NameType
UpurePure !0
UemptyEmpty !0
Rglobal[r:%].Global r
Rconst[r:%].Const r
Rmutable[r:%].Mutable r
Rlazy[r:%].Lazy r
Rdirect[r:%].Direct r
Uuse[r:%].Global r => Const r => Empty (Use r)
Uread[r:%].Const r => Pure (Read r)
Ualloc[r:%].Const r => Pure (Alloc r)
  • 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.
  • 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.
  • Only witnesses of types Pure t or Empty t can be joined, for some type t.

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.

ATYPE := VAR | CON | ( TYPE )

Examples

 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


History

  • 2009: Introduced a polymorphic witness join operator (&) instead of using join constructors MkJoinEffect and MkJoinClosure. These cluttered the core programs too much.
  • 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.