Encoding versus using an existential type when encoded as a universal

Question

I'm trying to better understand the nuances of encoding versus using an existential type after we transform it into a universal. In short, it appears to me that using an existential type is much easier than encoding one and I'll explain what that means to me below. To better explain this, let us start off with two rules from logic

1. ∀x.P(x) ⇒ ¬(∃x.¬P(x))
2. ∃x.P(x) ⇒ ¬(∀x.¬P(x))

From this, we have that

1. ∀x.(P(x) ⇒ Q)
2. ∀x.(¬P(x) ⩖ Q)
3. (∀x.¬P(x)) ⩖ Q
4. (¬¬(∀x.¬P(x))) ⩖ Q
5. (¬(¬(∀x.¬P(x)))) ⩖ Q
6. (¬(∃x.P(x))) ⩖ Q
7. (∃x.P(x)) ⇒ Q

Hence,

(∃x.P(x)) ⇒ Q = ∀x.(P(x) ⇒ Q).

In other words, if the first argument to a function is an existential, we can pull out the existential type to the left and represent it as a universal. This is what I'll call the use of an existential rule. Now, normally when people talk about the equivalence between a universal and existential type, we see

∃x.P(x) = ∀y.(∀x.P(x) ⇒ y) ⇒ y.

This is what I call the encoding of an existential rule. In order to see this equivalence, we have

1. ∀y.(∀x.P(x) ⇒ y) ⇒ y
2. ∀y.((∃x.P(x)) ⇒ y) ⇒ y
3. ∀y.¬((∃x.P(x)) ⇒ y) ⩖ y
4. ∀y.¬(¬(∃x.P(x)) ⩖ y) ⩖ y
5. ∀y.((∃x.P(x)) ⩕ ¬y) ⩖ y
6. ∀y.((∃x.P(x)) ⩖ y) ⩕ (y v ¬y)
7. ∀y.(∃x.P(x)) ⩖ y
8. (∃x.P(x)) ⩖ ∀y.y
9. ∃x.P(x)

Alright, so what this rule says to me is that an existential type is a function that accepts a program that converts P(x) to a y and then outputs a y.

Now, here's what I mean about the difference between using an existential and building an existential. Say we want to build a poor man's module in a language like OCaml, we can do so with a program like this

type 't mypackage = {
    add : 't * 't -> 't;
    fromInt : int -> 't;
    toString : 't -> string};;

let int_package  = {
    add  = (fun (x,y) -> x+y) ;
    fromInt = (fun x->x) ;
    toString = (fun x->string_of_int x)};;

let str_package  = {
    add  = (fun (x,y) -> x^y) ;
    fromInt = (fun x->string_of_int x) ;
    toString = (fun x-> x)};;

let simpleProg fns =
   let exp01 = fns.fromInt 1 in
   let exp02 = fns.fromInt 2 in
   let exp03 = fns.add (exp01,exp02) in
   fns.toString exp03

let _ = simpleProg int_package;;
let _ = simpleProg str_package;;

This uses the use of an existential rule from above. As far as types, we have

val int_package : int mypackage
val str_package : string mypackage
val simpleProg : 'a mypackage -> string = <fun>

Basically, we want to design a function called simpleProg : (∃x.mypackage(x)) ⇒ string. In order to do that, we instead build a function with the type ∀x.mypackage(x) ⇒ string and encode our package with a universal, which is straightforward to do in most functional languages. Now, if instead we wanted to actually encoding int_package and str_package as existential packages rather than universal packages, we use the encoding of an existential rule and we instead end up with the code like

type 't mypackage = {
    add : 't * 't -> 't;
    fromInt : int -> 't;
    toString : 't -> string};;

let apply (arg : 't mypackage) (f : 't mypackage -> 'u) : 'u =
    f arg;;

let int_package_ = {
    add  = (fun (x,y) -> x+y) ;
    fromInt = (fun x->x) ;
    toString = (fun x->string_of_int x)};; 

let int_package = apply int_package_;;

let str_package_  = {
    add  = (fun (x,y) -> x^y) ;
    fromInt = (fun x->string_of_int x) ;
    toString = (fun x-> x)};; 

let str_package = apply str_package_;;

let simpleProg_ fns =
   let exp01 = fns.fromInt 1 in
   let exp02 = fns.fromInt 2 in
   let exp03 = fns.add (exp01,exp02) in
   fns.toString exp03

(* Notice that we have inverted how we use the existentials here.  We give the
existential the program and don't give the program the existential *)
let _ = int_package simpleProg_;;
let _ = str_package simpleProg_;;

(* This flips things *)
let simpleProg fns =
    fns simpleProg_;;

let _ = simpleProg int_package;;
let _ = simpleProg str_package;;

Here, we have that

val int_package : (int mypackage -> '_a) -> '_a = <fun>
val str_package : (string mypackage -> '_a) -> '_a = <fun>

which is basically what we want. The int and string types are hidden inside of the packaging. Then, we see that

val simpleProg : (('a mypackage -> string) -> 'b) -> 'b = <fun>

which again is mostly what we want. Really, we kind of wanted

val simpleProg : (('a mypackage -> 'b) -> 'b) -> string = <fun>

but the type variables sort this out for us (or I've made a terrible mistake. One of the two.)

In any case, the constructions for actually creating an existential from a universal seem really heavy as the second program shows whereas the the constructions for using an existential seems pretty straightforward, which the first program shows. Basically, that's what I mean by using an existential is much easier than making one.

So, really, my two questions are:

1. If we only care about using existential packages in functions, is the encoding into universal types much easier than creating existential packages that sit independently? Assuming this is true, it seems that this is because we can just encode our existential package with a universal package (the type mypackage above.)
2. What do we ultimately lose if we restrict ourselves to just using the use of an existential rule and using these universal packages? Again, by universal package, I mean the trick with the type mypackage above.

---

Edit 1

camlspotter and Leo White were right that my types were exposed and the packages messed up. Here's a rewritten and very verbose version of the same code

(* Creates the type forall t.P(t) *)
type 't mypackage = {
    add : 't * 't -> 't;
    fromInt : int -> 't;
    toString : 't -> string};;

(* Creates the type forall u.(forall t.P(t) -> u) *)
type 'u program_that_takes_open_package_and_returns_u = {
    code : 't. 't mypackage -> 'u};;
(* Creates the type forall u.(forall t.P(t) -> u) -> u *)
type 'u applies_program_to_specified_packaged_and_produces_u =
    'u program_that_takes_open_package_and_returns_u -> 'u;;

(* Has type P(int) *)
let int_package = {
    add  = (fun (x,y) -> x+y) ;
    fromInt = (fun x->x) ;
    toString = (fun x->string_of_int x)};; 
(* Has type forall u.(forall.t P(t) -> u) -> u. *)
let (applies_prog_to_int_package :
        'u applies_program_to_specified_packaged_and_produces_u) =
    (* Has type forall u.(forall.t P(t) -> u) *)
    (* Even though we specify an int_package, the program must accept all
    packages *)
    fun (program:'u program_that_takes_open_package_and_returns_u) ->
        program.code int_package;;

(* Has type P(string) *)
let str_package  = {
    add  = (fun (x,y) -> x^y) ;
    fromInt = (fun x->string_of_int x) ;
    toString = (fun x-> x)};;
(* Has type forall u.(forall.t P(t) -> u) -> u. *)
let (applies_prog_to_str_package :
        'u applies_program_to_specified_packaged_and_produces_u) =
    (* Has type forall u.(forall.t P(t) -> u) *)
    (* Even though we specify an str_package, the program must accept all
    packages *)
    fun (program:'u program_that_takes_open_package_and_returns_u) ->
        program.code str_package_;;

(* The code of a program that takes a package called fns and produces a string *)
let simpleProg = { code = fun fns -> 
   let exp01 = fns.fromInt 1 in
   let exp02 = fns.fromInt 2 in
   let exp03 = fns.add (exp01,exp02) in
   fns.toString exp03}

(* Apply the program to each of the packages *)
let _ = applies_prog_to_int_package simpleProg;;
let _ = applies_prog_to_str_package simpleProg;;

(* Show that we can, in fact, keep all of the packages in a list *)
let _ = [applies_prog_to_int_package;applies_prog_to_str_package];;

I guess the biggest thing I learned in this process is essentially this reencoding trick inverts the order of how things are constructed. Essentially, these packages build up a process where they accept a program and then apply this program to their internal representation. By playing this trick, the internal type of the package is hidden. Although this is theoretically equivalent to the existential type, personally, I find the process different than a direct implementation of an existential as described by, for example, Pierce's Types and Programming Languages book.

In direct answer to my questions above

1. The universal package trick works and is much easier to implement if you're only interested in passing in a package directly to a function. It is absolutely not an existential package, but it's use is pretty similar to a true existential package used in this same context, but without the unpacking. By similar, I mean that we retain the ability to pass in different representations of a package, which is based on different types, into a function and then compute generically with these representations.
2. What we lose in these universal packages is the ability to treat these packages like true first class members. The simplest example is that we can't put a bunch of these universal packages into a list because their types are exposed. A true existential package hides the type and is therefore much easier to pass around a larger program.

Also, universal package is a terrible word. int_package and str_package are specialized, so they're not really universal. Mostly, I don't have a better name.

Answer 1

I do not really understand your questions, but your encoding of existential seems to be incorrect.

As you mentioned, if you want to mimic ∃'t. 't mypackage, then you have to create a type

∀'y. (∀'t. 't mypackage -> 'y) -> 'y

but this is not OCaml type ('t mypackage -> 'y) -> 'y which is, more precisely,

∀'y. ∀'t. ('t mypackage -> 'y) -> 'y

Look at the position of the quantifier.

OCaml's type schemes are left most quantified and it cannot have higher rank types like ∀'y. (∀'t. 't mypackage -> 'y) -> 'y, but we can mimic it with its record polymorphic fields:

type 'y packed = { unpacked : 't. 't mypackage -> 'y }  
(* mimicing ∀'t. 't mypackage -> 'y *)

with this type, the existential type can be implemented as

type 'y closed_package = 'y packed -> 'y 
(* mimicing a higher ranked type ∀'y. (∀'t. 't mypackage -> 'y) -> 'y,
   which is equivalent with ∃'t. 't mypackage *)

If you do not like the type variable 'y is exposed, you can hide it again with the record polymorphic field:

type really_closed_package = { l : 'y. 'y closed_package }

The package implementations can be packed into this interface as follows:

let closed_int_package = { l = fun packed -> packed.unpacked int_package }
let closed_str_package = { l = fun packed -> packed.unpacked str_package }

Since these packed versions have the same type, we can put them into a list:

let closed_packages = [ closed_int_package; closed_str_package ]

this is usually what we want to do with the existentials.

Now the encoding is complete. Using it also requires some complexity but rather trivial:

let doubled_int_string p x =
  let x = p.fromInt x in
  p.toString (p.add (x,x))

doubled_int_string is for opened packages and we cannot simply use it against the closed ones. We need some conversions:

let () =
  (* Using "universal" packages *)
  print_endline (double_int_string int_package 3);
  print_endline (double_int_string str_package 3);

  (* Equivalents using "existential" packages *)
  print_endline (closed_int_package.l { unpacked = doubled_int_string } 3);
  print_endline (closed_str_package.l { unpacked = doubled_int_string } 3)

Answer 2

As pointed out by camlspotter, your encoding is not quite correct it should instead use a type:

type 'k mypackage_cont = { p: 't. 't mypackage -> 'k } 

Then your encoded packages would have the types:

val int_package1 : 'k mypackage_cont -> 'k
val str_package1 : 'k mypackage_cont -> 'k

whereas your other versions have types:

val int_package2 : int mypackage
val str_package2 : string mypackage

Notice that the encoded version is truly existential because it does not mention the existential type (int or string) within its type. This is the key difference.

Consider, for example, creating a heterogeneous list. You can do that with the proper encoding:

# [ int_package1; str_package1; ];;
- : ('a mypackage_cont -> 'a) list = [<fun>; <fun>]

but not with the non-encoded version:

# [ int_package2; str_package2 ];;
Characters 16-28:
  [ int_package2; str_package2 ];;
                  ^^^^^^^^^^^^
Error: This expression has type string mypackage
       but an expression was expected of type int mypackage
       Type string is not compatible with type int 

Answer 3

Frankly this is over my head somewhat, but I get your basic idea, I think. There is something similar in Haskell for supporting existential types, as I recall.

However, the types for your second construction don't look so useful to me:

val int_package : (int mypackage -> '_a) -> '_a = <fun>

This is a monomorphic type, where _a is as yet unspecified. It's not a polymorphic type. This means you can only give it one type of program. If you write a second program that wants to return an int rather than a string, your existential package won't let you call it. At least, this is how it looks to me.

The first construct has a truly polymorphic type, so it seems like it should work better.

(A more knowledgeable type theory type person could probably offer more help :-)