Existential quantifiers in computation types

[matthewhammer]

Motivating Examples

Suppose we want to write the following type, for a function that internally chooses a way to subdivide a set of named natural numbers, and then exposes these two (disjoint) subsets in its output type:

partition : { 
     0 { Nat -> F Bool } -> 
     0 NatSet[X] -> 
   exists (Y1,Y2):NmSet | X=(Y1%Y2). 
     0 F (x NatSet[Y1] x NatSet[Y2]) 
 }

Today
We can write this type today, but only by expressing it this way, with the existential quantifier placed at the return type, which consists of a pair (a value type):

partition2 : { 
     0 { Nat -> F Bool } -> 
     0 NatSet[X] -> 
     0 F exists (Y1,Y2):NmSet | X=(Y1%Y2). 
        (x NatSet[Y1] x NatSet[Y2])
 }

While this "works", it is not a complete solution: The partition2 function only mentions the two subsets Y1 and Y2 in the return type, but not early enough to mention those subsets in its effects. So, this placement of the quantifier does not work if any effects concern one set but not the other, or if the effects somehow use these subsets differently (e.g., applying different name functions to each).

To overcome these issues, we need to distinguish these sets in the effects, and to do so, we need to mention these sets "earlier" in the function type, as in the first partition's type.

More examples:

• Transforming a named list into a named level tree
• Updating the invariant map, in Patchwork (static analysis framework)

Syntax (new form)

To write the first version above, we need to extend the form of E, written exists a:g|P.E, and read "Exists index (variable) a, with sort g, such that proposition P holds true, ...":

Effect, and computation type:
                      E ::= eff C 
                           |  exists a:g|P. E 
                           |  foralli a:g|P. E
                      eff ::= {W; R}
Computation type:
                      C ::= A -> E 
                          |  F A

Bidirectional typing (new rules)

Judgement form: Under G, expression e has effect and computation type E:
G |- e : E

Introduction form for exists (checking):

G |- X : g
G |- ([X/a]P) true
G |- e <==  C
------------------------------------- :: exists/intro/check
G |-  pack X ; e <== exists a:g | P. C

Elim form for exists (checking):

G |- e1 ==> exists a:g | P. F A
G, a:g, P true, x:A |- e2 <==  E2
---------------------------------- :: exists/elim/check
G |-  let x = e1 ; e2 <== E2