quantifier-syntax.md

Quantifiers

Idea: create a surface syntax where all quantifiers behave more like records/modules with labelled entries.

Examples

{
  out id : {
    all A : Type,
    in a : A,
    out a' : A,
  },
  out const : {
    all A : Type,
    all B : Type,
    in a : A,
    in b : B,
    out a' : A,
  },
}

Σ(id : ∀(A : Type). Π(a : A). Σ(a' : A). Unit).
  Σ(const : ∀(A : Type). ∀(B : Type). Π(a : A). Π(b : B). Σ(a' : A). Unit).
    Unit

Surface language

surface.type ::=
  | ident
  | 'Type'
  | '{' (surface.decl ',')* surface.decl? '}'

surface.decl ::=
  | 'in' ident ':' surface.type
  | 'out' ident ':' surface.type
  | 'all' ident ':' surface.type
  | 'some' ident ':' surface.type

Core language

core.type ::=
  | ident
  | 'Type'
  | 'Unit'
  | 'Π' '(' ident ':' core.type ')' '.' core.type
  | 'Σ' '(' ident ':' core.type ')' '.' core.type
  | '∀' '(' ident ':' core.type ')' '.' core.type
  | '∃' '(' ident ':' core.type ')' '.' core.type

Elaboration

elaborate : surface.type -> core.type
elaborate (ident : ident) = ident
elaborate 'Type' = 'Type'
elaborate ('{' '}') = 'Unit'
elaborate ('{' decl ',' (decls : _* _?) '}') =
  elaborate decl (elaborate ('{' decls '}'))

elaborate : surface.decl -> core.type -> core.type
elaborate ('in' ident ':' type1) type2 = 'Π' '(' ident ':' type1 ')' '.' type2
elaborate ('out' ident ':' type1) type2 = 'Σ' '(' ident ':' type1 ')' '.' type2
elaborate ('all' ident ':' type1) type2 = '∀' '(' ident ':' type1 ')' '.' type2
elaborate ('some' ident ':' type1) type2 = '∃' '(' ident ':' type1 ')' '.' type2

Todo

• Allow for permuting the order of fields

• Make common constructions less verbose (eg. for functions):

  id : { A, a : A } => A
  const : { A, B, a: A, b: B } => A
  

  id : {
    in A : Type,
    in a : A,
    out return : A,
  }
  
  const : {
    in A : Type,
    in a : A,
    in b : B,
    out return : A,
  }
  

• Add row-style operations: eg. merging, adding, renaming, removing fields

• Add field lookups

• Add record terms

• Mutual recursion

• Manifest fields/singleton types

• Inductive types

• Generative modules

• Implicit/instance arguments

• Data (aka. values) vs Codata (aka. actions/computations)

• Resolve bundled vs. unbundled structures.

  • Idea: input applications reduce to records (so that the arguments can be projected on after-the-fact), rather than a single output. Might need to handle destructive inputs for functions however (in the common, non-module case).

• Strong vs. weak sums???

Equivalences

{ in l1 : T1, in l2 : T2, ... } = { in l2 : T2, in l1 : T1, ... }
{ out l1 : T1, out l2 : T2, ... } = { out l2 : T2, out l1 : T1, ... }

Resources

• Quantification
• Universals to the right, Existentials to the left: the adjoint triple "Exists ⊣ Const ⊣ Forall"