We describe various ways of eliminating explicit existential quantification in data types, replacing such data types with isomorphic structures. We stress the encoding of existentials in terms of *equivalent simple, first-order types*. All the techniques let us work with existentials in a language like OCaml, which does not support existentials directly.

- Introduction and motivation
- Eliminating simple existentials
- Eliminating existential packages
- Eliminating recursive existential variants
- Eliminating translucent existentials

Representing existentials via isomorphic complex types (for contrast with the above)

- Existential types
`exists a. t`

along with universal types`forall a. t`

are two well-known examples of second-order types. Universals represent type parameterization and so are used to give type to parametrically polymorphic functions such as the identity function. Existentials express type abstraction; their typical application is typing abstract data types, objects, and implicitly heterogeneous lists.A sample existential type

`exists a b. (a,b)`

is the type of*any*pair whatsoever. We can take the pair apart using`fst`

and`snd`

, put it back together. We can pass the components of the pair around, but we cannot do anything else with them: we do not know their exact types and so have no idea what operations may apply to them. Existential types are supported as a widely implemented extension to Haskell98. In Haskell, our sample data type is declared as`data Pair = forall a b. Pair a b`

(using the`forall`

quantifier, which may be confusing at first).Existentials are most known as an implementation technique for abstract data types, aka packages. Packages are data structures whose realization is hidden and which can be manipulated only by a closed set of pre-defined operations. In other words, packages expose the interface but hide the implementation. One of the simplest packages is

data SE = forall x. SE x (x -> String)

consisting of a value of*some*type`x`

and a single pre-defined operation to manipulate this value, namely, to observe this value as a`String`

. We can declare the package differently, but equivalently asdata SE' = forall x. Show x => SE' x

using so-called bounded quantification, where the unknown type`x`

is assured to be a member of the type class`Show`

. The two declarations are equivalent; we can always convert the declaration with the type-class qualified quantification into the declaration with the unrestricted quantification by including all the type class methods (such as`show :: x -> String`

) as explicit operations of the package. Therefore, we do not consider bounded quantification any further on this page.We can define two values of our existential type

se1 = SE (5::Int) show se2 = SE "xx" id tle = [se1, se2] tle_run = map (\(SE x f) -> f x) tle

Although the two values represent the type`x`

differently,`Int`

vs.`String`

, the difference is abstracted over and so the two values have the same type,`SE`

. Therefore, the two values can be placed into the same list and uniformly manipulated. We thus observe the other, related benefit of existentials: supporting implicitly heterogeneous lists -- lists of elements of different types but with a common set of operations. In the above example we relied on existentials to `place' an`Int`

and a`String`

in the same list, and map the common `to-string' operation over the list. Existentials are only one of several ways of implementing implicitly heterogeneous lists; the others are described elsewhere on this web page. **References**- John C. Mitchell, Gordon D. Plotkin: Abstract types have existential type.

ACM Transactions on Programming Languages and Systems, 1988.

< http://theory.stanford.edu/people/jcm/papers/mitch-plotkin-88.pdf >Luca Cardelli: Type systems.

The Computer Science and Engineering Handbook (Allen B. Tucker (Ed.)). CRC Press, 2004. Chapter 97.

< http://lucacardelli.name/Papers/TypeSystems.pdf >

- In the introduction section we used existential to define a trivial abstract data type with a single operation of observing the hidden, abstract value as a
`String`

.data SE = forall x. SE x (x -> String)

By pattern-matching the value of the existential against the pattern

`(SE x f)`

we can get hold of the value`x`

of the abstracted type and pass the value around. The only non-trivial operation possible on`x`

is applying to`x`

the function`f`

obtained as the result of the*same*pattern-match operation. One may wonder therefore why not to apply`f`

to`x`

from the outset and so to observe`x`

right away. There is nothing to hide any more and we do not need any existentials.The gist of eliminating an existential is representing it by a tuple of its possible observations. We represent

`SE`

as a simple data typedata S1 = S1 String

In a non-strict language like Haskell, the observation, the`String`

, is not computed unless needed. In a strict language such as OCaml, we should use thunks to delay computations, and so we represent`SE`

as`type s1 = unit -> string`

. The implicitly heterogeneous list of an`Int`

and a`String`

with the common `to-string' operation, cf.`tle`

above, can be written in Haskell simply asts1 = [S1 (show 5), S1 "xx"] ts1_run = map (\(S1 x) -> x) ts1

or as following in OCamllet ts1 = [(fun () -> string_of_int 5); (fun () -> "xx")] List.map (fun f -> f ()) ts1

To prove that

`SE`

and`S1`

are equivalent, we exhibit the following total functions to convert the value of one type to the other:iso_SES1 :: SE -> S1 iso_SES1 (SE x to_string) = S1 (to_string x) iso_S1SE :: S1 -> SE iso_S1SE (S1 s) = SE () (\() -> s)

It is clear that the composition`iso_SES1 . iso_S1SE :: S1 -> S1`

is the identity. Proving that there is no context that can distinguish a value`tse::SE`

from the value`(iso_SES1 . iso_S1SE) tse`

is more involved. We have to appeal to the opacity of the existentially quantified type. The technique of Sumii and Pierce seems best for such equivalence proofs. **References**- Eijiro Sumii and Benjamin C. Pierce: A Bisimulation for Type Abstraction and Recursion.

Journal of the ACM, vol. 54, issue 5, article 26, pp. 1-43, October 2007.

The paper presents ``a bisimulation method for proving the contextual equivalence of packages in lambda-calculus with full existential and recursive types.'' Unlike other bisimulations, it is complete even for existential types.

- A package packs a value of an abstract type together with a set of operations to manipulate the value. Since the type of the value is abstract, the value can only be manipulated by the operations of the same package. Here is a typical package, described as an OCaml module type:
module type COUNTER = sig type t val init : unit -> t val observe : t -> int val step : t -> t end

The package interface introduces an abstract type`t`

of an unknown representation and three operations: the producer, the observer, and the transformer. The producer makes instances of the counter in the initial state; the step operation advances the counter. We can also observe the current value of the counter. Our package is not an OCaml value. With the exception of MoscowML and AliceML, modules are not first-class values in ML and cannot be passed around or stored in lists.To implement packages in the language itself, one commonly uses existentials -- which are not directly supported in OCaml. Nevertheless, we are able to realize packages as first-class values in ML or other simply-typed language with data types. By the very definition of a package, its set of operations is pre-defined and closed. We can enumerate the possible observations, thus eliminating the existential by replacing it with the tuple of its possible observations.

type counter = C of (unit -> int) * (unit -> counter)

We represent the package `counter' as a tuple of the observed current value of the counter and the advanced counter. These are the only possible observations of a counter. Thunks delay the observations until their results are required. Here are two counters with two different internal states, a pair of integers vs. a floating-point number:let counter1 = (* internal function, unavailable outside *) let rec make seed upper = C ((fun () -> seed), (fun () -> let seed = if seed >= upper then 0 else succ seed in make seed upper)) in make 0 5 let counter2 = (* internal function, unavailable outside *) let observe seed = int_of_float (10.0 *. seed) in let step seed = cos seed in let rec make seed = C ((fun () -> observe seed), (fun () -> make (step seed))) in make 0.0

We can place the two counters into the same list and iterate over:let lst = [counter1; counter2];; let advance_all = List.map (function C (_,adv) -> adv ());; let show_all = List.iter (function C (s,_) -> Printf.printf "%d\n" (s()));; let test = let () = show_all lst in let () = show_all (advance_all (advance_all lst)) in ();;

We thus demonstrated a very old idea -- whose realization in 1976 was the birth of Scheme -- that closures are poor-man objects.

More generally, we can describe a package as the following Haskell existential data type:

data CE i m o = forall x. CE x -- current state (i -> x) -- producer (x -> m -> x) -- transformer (`step') (x -> o) -- observer

Here, the type`i`

is the type of the arguments to the constructor; the type`m`

describes the additional arguments to the transformer, and`o`

is the type of observations. The corresponding simple data type isdata C1 m o = C1 (m -> C1 m o) o

To show the isomorphism between the existential package and the existential-free representation, we exhibit the following pair of total functions. The function`iso_CEC1`

converts the existential data type`CE`

into a pair of the corresponding simple data type`C1`

and the constructor function. The latter creates the (initial) value of`C1`

. The function`iso_C1CE`

is the observational inverse.iso_CEC1 :: CE i m o -> (C1 m o, i -> C1 m o) iso_CEC1 (CE x init step observe) = (makeC1 x, \i -> makeC1 (init i)) where makeC1 x = C1 (makeC1 . step x) (observe x) iso_C1CE :: (C1 m o, i -> C1 m o) -> CE i m o iso_C1CE (c1, makeC1) = CE c1 init step observe where init = makeC1 step (C1 step1 _) = step1 observe (C1 _ obs1) = obs1

One may call`C1 m o`

the Skolem function for the quantified type variable`x`

. **Version**- The current version is 1.3, June 28, 2008.
**References**- In the final form, the idea of using the recursive first-order data type was explained in the message Eliminating existentials, finally posted on the Caml list on Wed, 14 Nov 2007 00:37:10 -0800 (PST). The early version of the idea was discussed in the thread ``Using existential types'' on Haskell-Cafe in October 2003.
Bernhard Beckert and Joachim Posegga: leanTAP: Lean Tableau-based Deduction.

Journal of Automated Reasoning, v15, N3, pp. 339-358, 1995.

Taking a formula itself as the Skolem-term is used in the leanTAP theorem prover. The authors credit Hilbert and Bernays, 1939.

- Existentials also prove useful in embedding domain-specific languages, including monadic languages. Here is a sample representation of a trivial first-order language with application:
data Expr a = Val a | forall b. Apply (Expr (b->a)) (Expr b) ex1 = Apply (Val fromEnum) (Apply (Apply (Val (==)) (Val 'd')) (Val 'c'))

`Expr a`

describes the result of zero or more applications as well as the structure of this series of applications. Jan-Willem Maessen observed that the two aspects can be represented separately, in the following existential-free data type:data E1 a = E1 a Tree data Tree = Leaf | Node Tree Tree

We again exhibit a pair of total functions to convert between the two data types:

iso_EXE1 :: Expr a -> E1 a iso_EXE1 (Val v) = E1 v Leaf iso_EXE1 (Apply opr opa) = E1 (opr' opa') (Node tr ta) where E1 opr' tr = iso_EXE1 opr E1 opa' ta = iso_EXE1 opa iso_E1EX :: E1 a -> Expr a iso_E1EX (E1 v Leaf) = Val v iso_E1EX (E1 v (Node t1 t2)) = Apply (iso_E1EX (E1 (\() -> v) t1)) (iso_E1EX (E1 () t2))

**References**- The first-order representation given here first appeared as the last encoding in the message

Jan-Willem Maessen: Using existential types

posted on Haskell-Cafe on Fri Oct 10 16:57:12 EDT 2003.

The whole discussion thread is also relevant. No attempt to establish isomorphism was made back then.

- Some existentials are translucent, exposing part of their internal structure. The epitome of such existentials was given by Chung-chieh Shan:
data LE = forall x. LE [x] ([x] -> String)

This data type exposes the list as part of

`LE`

and the number of elements in the list, while hiding all information about the elements themselves. There are no operations to examine the elements individually; in particular, we cannot compare the elements. We cannot tell if the list contains duplicates. We can do only three sorts of observations on`LE`

: (i) observe the number of elements in the list, the first component of`LE`

; (ii) observe the current `state', by applying the second component of`LE`

to the first component; (iii) transform the first component to a different list and then observe the result. When transforming the list, we cannot examine the elements, but we may arbitrarily permute, drop and duplicate the elements. The permissible transformations then are scramblings of the list. Thus the data type LE is equivalent to the following package:data LEP = forall xs. LEP xs -- current state, hidden (n::Int) -- the exposed part of the curr state (xs -> (forall a. [a]^n->[a]) -> xs) -- transformer (xs -> String) -- observer

One may think that scramblings can be described by a type

`(forall a. [a] -> [a])`

, but this is not precise. The set of transformations depends on the size of the list. For example, the only possible `scrambling' of the empty list is the identity: We cannot create any new elements of the list, and we are given no elements to drop or replicate. If the first component of`LE`

is the list of one element, we could either drop or arbitrarily replicate this one element, producing lists of any size all containing copies of that one element. Generally, if the first component of`LE`

is the list of`n`

elements, we may regard these elements as a set of distinct `letters', the alphabet`Sigma`

. The scramblings then map`Sigma`

to`Sigma*`

, to all strings over the alphabet`Sigma`

. Thus we need the*dependent type*`[a]`

, denoting a list of elements of the type^{n}`a`

and the length`n`

.Using the general technique of representing an existential package by the set of available observations, we can derive the equivalent first-order data type

data L1P = L1P (n::Int) (forall a. [a]^n->[a]) -> String String

The second component of`L1P`

maps each possible scrambling on the list of`n`

distinct elements to a string. It is clear that we need the precise characterization of scramblings if we wish to establish the isomorphism of`L1P`

with`LE`

. The non-dependent type`(forall a. [a]->[a])`

is just `too large'.Because of the dependent type, neither

`LEP`

nor`L1P`

can be written in Haskell, at least not directly. Chung-chieh Shan showed the way around. We*can*write the type of scramblings of the list of`n`

elements, as a*nested*data type. Recall that the set of scramblings is the set of all strings over the alphabet of`n`

distinct letters. We can write the type of the alphabet as follows: the type`()`

represents the singleton set, with one element`()`

. The type`Maybe ()`

then represents a set with two elements,`Nothing`

and`Just ()`

;`Maybe (Maybe ())`

represents a set with exactly three elements:`Nothing`

,`Just Nothing`

,`Just (Just ())`

. Then all scramblings for the list of three elements are precisely described by the set of (non-bottom) values of the type`[Maybe (Maybe ())]`

. For example, the identity scamble is represented as`[Nothing, Just Nothing, Just (Just ())]`

; the scamble that drops the last element and replaces it with the first element is`[Nothing, Just Nothing, Nothing]`

, etc. Thus`Maybe`

represents the alphabet of exactly^{(n-1)}()`n`

elements, and the type`[Maybe`

precisely represents the set of all possible strings over that alphabet. That is, there exists a 1-1 correspondence between a non-bottom value of the type^{(n-1)}()]`Maybe`

and a string over the^{(n-1)}()`n`

-letter alphabet.The following is a simple embellishment of the code originally written by Chung-chieh Shan in December 2003. It builds the encoding of the alphabet and of the above correspondence. For example, the list of three elements of the unknown type is represented by the list of their 'codes':

`[Nothing, Just Nothing, Just (Just ())]`

.-- First-order representation, via a nested data type data L1 = Lempty String | Lmany (Ln ()) data Ln a = Ln ([a] -> String) | Ln1 (Ln (Maybe a)) iso_LEL1 :: LE -> L1 iso_LEL1 (LE [] to_string) = Lempty (to_string []) iso_LEL1 (LE (x:xs) to_string) = Lmany (build to_string xs [x] [()]) where build :: Eq a => ([x] -> String) -> [x] -> [x] -> [a] -> Ln a build tos [] xs codes = Ln (tos . map (encode xs (reverse codes))) build tos (x:t) xs codes = Ln1 (build tos t (x:xs) (Nothing:map Just codes)) encode xs codes y = maybe (error "can't happen") id $ lookup y (zip codes xs) iso_L1LE :: L1 -> LE iso_L1LE (Lempty s) = LE ([]::[()]) (const s) iso_L1LE (Lmany ls) = make ls [()] where make :: Ln a -> [a] -> LE make (Ln f) codes = LE codes f make (Ln1 ls) codes = make ls (Nothing:map Just codes) -- test the equivalence of two LE values on sample points test_eqLE (LE xs1 obs1) (LE xs2 obs2) = zip (map obs1 (tails xs1)) (map obs2 (tails xs2)) test_LE1E = test_eqLE anLE (iso_L1LE . iso_LEL1 $ anLE) where anLE = LE "abc" reverse test_LE1E' = test_eqLE anLE (iso_L1LE . iso_LEL1 $ anLE) where anLE = LE "abc" (drop 1)

- A common problem is the uniform manipulation of a collection of elements that do not have the same type but permit a common set of operations. For example, a GUI form may include several widgets -- scrollbars, buttons, text entry fields -- of different structure and generally of different types. These child widgets share common operations such as repositioning, redrawing, showing and hiding. A typical implementation of the GUI form includes a list of the child widgets, and functions to iterate over the list, e.g., to show all widgets.
To place elements of different types into the same homogeneous list we have to inject the elements into the appropriate union type (the universe). Variant types are the simplest way to build the universe. For example,

type univ = VInt of int | VFloat of float | VBool of bool

lets us place integers, floating-point numbers and booleans into the same list:`[VInt 1; VFloat 2.0; VBool false]`

. The variant type has the clear disadvantage of being non-extensible. One often needs*open unions*.Existentials are one way of building open unions, with an advantage of type abstraction. If encapsulation is not required, one can always build open unions in other ways. For example, ML supports open unions in the form of exception types. OCaml has polymorphic open unions. Even simpler, the type of mutable cells is an open union!

Yet another way of building open unions is by iterating the sum type. Here is an example in Haskell:

data Sum a b = InL a | InR b instance (Show a, Show b) => Show (Sum a b) where show (InL x) = show x show (InR x) = show x ex_sum = [InL (1::Int), InR (InL (2.0::Float)), InR (InR False)] test_sum = map show ex_sum -- ["1","2.0","False"]

One may define type classes for other common operations on the elements of`ex_sum`

. Building such lists by hand is inconvenient. OOHaskell demonstrates automatic iterated sums with the corresponding injection and projection operations.Implicitly heterogeneous lists without existentials offer no value abstraction, let alone type abstraction. On the upside, open unions support a projection operation, aka safe downcast.

**References**- The MLton team: UniversalType

< http://mlton.org/UniversalType >

The detailed explanation of implementing open unions in SML in terms of exceptions or reference cells.

- This approach is beside our goal of representing existentials in simple types: universals are not simple types, they are too of higher rank. We consider this well-known encoding for contrast.
data ShowableE = forall x. ShowableE x (x -> String) tle = [ShowableE 5 show, ShowableE "x" id] tle_run = map (\(ShowableE x f) -> f x) tle newtype ShowableU = ShowableU (forall w. (forall x. (x,x->String) -> w) -> w) tlu = [ShowableU (\k -> k (5::Int, show)), ShowableU (\k -> k ("x", id))] tlu_run = map (\(ShowableU k) -> k (\(x,f) -> f x)) tlu

Here,`ShowableE`

is a simple existential (the value of*some*type packed along with the function to show it), and`ShowableU`

is the corresponding universal: the wrapper over the polymorphic function that takes as an argument a polymorphic function`(forall a. (a,a->String) -> w)`

. The expressions`tle_run`

and`tlu_run`

both evaluate to the same result,`["5","x"]`

.Derek Elkins has lucidly explained the transformation as classical double-negation:

exists x. P x <=> ~~(exists x. P x) <=> ~(forall x. ~(P x)) <=> ~(forall x. P x -> _|_) <=> (forall x. P x -> _|_) -> _|_

where`~A`

means the negation of the formula`A`

and`_|_`

means `bottom' or falsity. **References**- Benjamin C. Pierce: Types and Programming Languages (MIT Press, 2002). Section 24.3
Derek Elkins: Re: Using existential types

A message posted on the Haskell-Cafe mailing list on Tue, 14 Oct 2003 03:49:32 -0400

- This approach is too beside our goal of representing existentials in simple types. Object types are implicitly existential, with respect to the types of their private fields. The very motivation for objects is the encapsulation of their state, which includes the abstraction over the types of their private fields so to prevent the outsiders from finding out not only the values of the fields but also their types. Outsiders should only use the methods of the object and should know nothing about object's fields.
We use the familiar `counter' as an illustration. We first declare the interface, the object type, for the sake of (optional) type annotations and clarity:

class type counter = object ('self) method observe : int method step : unit -> 'self end;;

We introduce two objects of the type`counter`

-- two implementations of the above interface. The two counters differ in their internal state: a pair of integers vs. a floating-point number.let counter1 = object val seed = 0 val upper = 5 method observe = seed method step () = let new_seed = if seed >= upper then 0 else succ seed in {< seed = new_seed >} end;; let counter2 : counter = object val seed = 0.0 method observe = int_of_float (10.0 *. seed) method step () = {< seed = cos seed >} end;;

The state of the objects is not directly observable. Therefore, despite the different type of the internal state, the two counters have the same type. We can put the counters in the same list and uniformly process them by iterating over the list.

let lst = [counter1; counter2];; let advance_all = List.map (fun c -> c#step ());; let show_all = List.iter (fun c -> Printf.printf "%d\n" c#observe);; let test = let () = show_all lst in let () = show_all (advance_all (advance_all lst)) in ();;

The test prints

`0 0 2 5`

**Version**- The current version is 1.1, Feb 18, 2008.
**References**- The code was originally posted in a message Re: existentials [was: Formal specifications of programming languages] on the Caml mailing list on Tue, 19 Feb 2008 00:54:23 -0800 (PST)
Didier Re'my: Programming Objects with ML-ART: An extension to ML with Abstract and Record Types.

International Symposium on Theoretical Aspects of Computer Software, 1994, LNCS 789, pp. 321-346.

The paper is the best exposition of the motivation and the design of objects in OCaml. The paper discusses existentials and type abstraction in great detail.Moscow ML: a light-weight implementation of Standard ML (SML)

< http://www.itu.dk/people/sestoft/mosml.html >

MoscowML has first-class modules, letting us `package' a module hiding the implementation details. The package is a first-class value and can be placed into lists and passed around.

oleg-at-okmij.org

Your comments, problem reports, questions are very welcome!

Converted from HSXML by HSXML->HTML