Existential types

[vmvasconcelos]

Let us start with an universal type

type T = (∀ a. ! a) ; Close

and write a consumer for T:

f : T -> ∀b . b -> ()
f c x = close (send x (sendType b c))

Intutively a session-∀ is associated with sendType. For universal types in general, we need

f c x = close (send x (<apply b to c>))

for which we already have syntax

f c x = close (send x (c @ b))

Kekkyoku: Universal types are universal types and so we may (must?) not distinguish the case of a session-∀ from an arbitrary-∀.
[Parenthesis. Do we need a @|> operator to sequence channel operations?

f c x = c @|> b |> send x |> close

End of parenthesis.]

Let us now consider the dual of T (now denoted by Dual T), that is, the type (∃ a. ! a) ; Wait, and write a consumer for it.

g : Dual T -> ()
g c =
  let {b, c} = receiveType c in -- b is a type variable
  let (x, c) = receive c in wait c -- x is of type b

I am assuming that b is unrestricted, of kind *T, so that x can be discarded.
Unlike sendType that can be understood as type application, receiveType requires four parameters. In let {a, x} = receiveType e1 in e2,

• e1 is an expression of type ∃ b. T
• a is a type variable standing for the type "in transit in the channel"
• x : a is a term variables standing for the continuation channel and
• e2 is where a and x are used (the scope of these variables)

In the functional world, existential types are used to describe packages. A type ∃ a. T describes a package T (for example, a record of queue operations) and a describes the type supporting the package (the representation, for example, a list of integer values). To open or import a package, Harper uses the syntax

open e1 as a with x in e2

Transforming open into receiveType we get

receiveType e1 as a with x in e2

which is somewhat difficult to read. Pierce instead uses the syntax

let {a, x} = e1 in e2

which is closer to the above proposal. (Pierce also suggests open e1 as {a, x} in e2. At this point it is worth rereading Chapter 24.)

My difficulty with this syntax is that the I and the O are misaligned. For the former we have a receiveType expression. For the latter a good old type application (in place of a sendType). Ideas?

The typing rule for the elimination of the existential type is that of Harper, adapted to the linear setting and to kinded type-variables:

Δ Γ1 |- e1 : ∃ a:k. T      Δ,a:k Γ2,x:T |- e2 : T2      Δ |- T2 : k'
--------------------------------------------------------------------- ∃-Elim
      Δ Γ1,Γ2 |- let {a, x} = receiveType e2 in e1 : T2

The Δ |- T2 : _ makes sure that T2 does not depend on a. This premise may be replaced by a not free in T2, because by agreement we have Δ,a:k |- T2 : k' and by strengthening we get Δ |- T2 : k'.

Reduction incorporates the idea of type-passing:

(νxy)( E1[x @ T] | E2[let {a, z} = receiveType y in e] ) -->
    (νxy)( E1[x] | E2[e[T/a][y/z] )

Let us go back to the function that consumes type (∃ a. ! a) ; Wait. Function g discards the value received. Suppose instead that we'd like to return the value, as in

g' c =
  let {b, c} = receiveType c in
  let (x, c) = receive c in (wait c ; x)

What would be the type of g'? It can't certainly be ∀ a . (∃ a. ! a) ; Wait -> a, for this type is alpha-congruent to ∀ b . (∃ a. ! a) ; Wait -> b where it is clear that a and b are unrelated. This is the reason for the 3rd premise in rule ∃-Elim. If x cannot be returned, then it must be consumed within the function.

[To be continued]

[gatpsilva]

My difficulty with this syntax is that the I and the O are misaligned. For the former we have a receiveType expression. For the latter a good old type application (in place of a sendType). Ideas?

I think this may be hard to avoid, and the syntax does not look too bad to me. But something comes to mind anyway... if good old type applications make sense in the context of sessions, then maybe so do good old type abstractions?

A sketchy idea, perhaps ridiculous: following the notion of let as a derived form, let {a, x} = receiveType e2 in e1 could be decomposed to something like (\\b -> \x -> [b/a]e1) @ e2. The idea here is that if the @ can interface with type output on its left, why not interface with type input on its right too? Here, it would first receive a type from e2 and pass it to the type abstraction, and then pass the resulting continuation to the inner term abstraction. This kind of resonates with (but is not really) the encoding of existentials as universals: "an existential package is thought of as a data value that, given a result type and a continuation, calls the continuation to yield a final result.", i.e., let {a,x} = e2 in e1 can be encoded as e2 @T2 (\\a -> \x . e1). Would something like this also make sense?