Implement simple demonstration of encoding existential types in terms of polymorphism

Author: sColin16

example/example.ml

@@ -1,5 +1,6 @@
 module Boolean = Boolean
 module ExampleHelpers = ExampleHelpers
+module Existential = Existential
 module Mixed = Mixed
 module ModularArithmetic = ModularArithmetic
 module Polymorphism = Polymorphism

example/existential.ml

@@ -0,0 +1,75 @@
+open Metatypes
+open TypeOperations.MapType
+open ExampleHelpers
+open Recursive
+
+(* TODO: create some helper functions to make existential encoding easier to use *)
+
+let new_label = typed_term (Const "new")
+let get_label = typed_term (Const "get")
+let inc_label = typed_term (Const "inc")
+
+(* Represents the type `CounterModule = {new: Counter, get: Counter -> Nat, inc: Counter -> Counter}` *)
+let counter_module =
+  map_type
+    (fun int ->
+      [
+        Intersection
+          [
+            (new_label.rtype.union, [ UnivTypeVar 0 ]);
+            ( get_label.rtype.union,
+              [ Intersection [ ([ UnivTypeVar 0 ], int) ] ] );
+            ( inc_label.rtype.union,
+              [ Intersection [ ([ UnivTypeVar 0 ], [ UnivTypeVar 0 ]) ] ] );
+          ];
+      ])
+    ind_integer
+
+(* Represents `forall Counter. (CounterModule -> Y)`, the "continuation" at the
+   core of the polymorphic encoding of existential types *)
+let counter_continuation =
+  map_type
+    (fun counter_module_union ->
+      [
+        UnivQuantification
+          [ Intersection [ (counter_module_union, [ UnivTypeVar 1 ]) ] ];
+      ])
+    counter_module
+
+(*
+  Represents the existential package type:
+  `{exists Counter, CounterModule}`
+  encoded using polymoprhism as:
+  `forall Y.((forall Counter.(CounterModule -> Y) -> Y)`
+*)
+let counter_package_type =
+  map_type
+    (fun counter_continuation_union ->
+      [
+        UnivQuantification
+          [ Intersection [ (counter_continuation_union, [ UnivTypeVar 0 ]) ] ];
+      ])
+    counter_continuation
+
+(* Term representing a counter ADT, encoded using polymoprhism, using Int as the implementation for Counter *)
+let counter_adt =
+  typed_term
+    (UnivQuantifier
+       (Abstraction
+          [
+            ( counter_continuation,
+              Application
+                ( UnivApplication (Variable 0, ind_integer),
+                  Abstraction
+                    [
+                      (new_label.rtype, one.term);
+                      ( get_label.rtype,
+                        Abstraction [ (ind_integer, Variable 0) ] );
+                      ( inc_label.rtype,
+                        Abstraction
+                          [
+                            ( ind_integer,
+                              Application (increment.term, Variable 0) );
+                          ] );
+                    ] ) );
+          ]))

test/dune

@@ -1,5 +1,5 @@
 (tests
- (names base boolean mixed modularArithmetic polymorphism recursive unions)
+ (names base boolean existential mixed modularArithmetic polymorphism recursive unions)
  (libraries setTypedLambda setTypedLambdaExample))
 
 (env

test/existential.ml

@@ -0,0 +1,45 @@
+open SetTypedLambdaExample.Existential
+open SetTypedLambdaExample.Recursive
+open SetTypedLambdaExample.ExampleHelpers
+open TypeOperations.Subtype
+open TestHelpers
+
+let get_new_counter =
+  typed_term
+    (Application
+       ( UnivApplication (counter_adt.term, ind_integer),
+         UnivQuantifier
+           (Abstraction
+              [
+                ( counter_module,
+                  Application
+                    ( Application (Variable 0, get_label.term),
+                      Application (Variable 0, new_label.term) ) );
+              ]) ))
+
+let get_incremented_counter =
+  typed_term
+    (Application
+       ( UnivApplication (counter_adt.term, ind_integer),
+         UnivQuantifier
+           (Abstraction
+              [
+                ( counter_module,
+                  Application
+                    ( Application (Variable 0, get_label.term),
+                      Application
+                        ( Application (Variable 0, inc_label.term),
+                          Application (Variable 0, new_label.term) ) ) );
+              ]) ))
+
+let () =
+  test "Counter ADT has expected type"
+    (is_subtype counter_adt.rtype counter_package_type)
+
+let () =
+  test "Get new counter evaluates to 1"
+    (evaluates_to get_new_counter.term one.term)
+
+let () =
+  test "Get incremented counter evaluates to 2"
+    (evaluates_to get_incremented_counter.term two.term)