Existential Types in Turmeric

This guide covers existential types: how to hide a concrete type behind an opaque boundary while still allowing operations on it through typeclass constraints. Existentials are the dual of higher-ranked types (forall): where forall lets the caller pick the type, exists lets the callee pick the type and only expose what the caller is allowed to do with it.

What is an existential type?

(exists [a] T) means "there is some type a for which T holds, but the value's holder does not know which one". The type is sealed behind the existential boundary. Without constraints the holder can do nothing useful with the inner value -- it is fully opaque.

With a typeclass constraint, the holder can call the constraint's methods on the inner value without ever learning its concrete type:

; A boxed value paired with an evidence that its type implements Show.
(exists [a] [(Show a)] a)

pack -- introduce an existential

(pack value (exists [a] [(C a) ...] T)) boxes a value as an existential. The compiler verifies at the pack site that the concrete type of value has an instance for each constraint (C a). The resulting record carries the boxed value and a vtable pointer for each constraint.

(defclass Show [a]
  (show [x] :cstr))

(definstance Show [int]
  (show [x] :cstr
    ```c
    char *buf = (char *)malloc(24);
    snprintf(buf, 24, "%lld", (long long)x);
    return (const char *)buf;
    ```))

(defn main [] :int
  (let [e (pack 42 (exists [a] [(Show a)] a))]
    0))

If you omit the constraint, the existential has no usable methods -- it is a pure information-hiding boundary:

(pack 42 (exists [a] a))   ; opaque -- nothing you can do with the inner value

open -- eliminate an existential

(open e [a v] body) unboxes the existential and binds:

The escape check then refuses any body whose result type can refer to a. That is what makes the existential genuinely opaque: you cannot return the inner value, alias it through a let, or smuggle it through one branch of an if.

; ok: body returns a :cstr, not a value of type `a`.
(open e [a v]
  (.show v))

; rejected: body would leak the abstract type `a` out of its scope.
(open e [a v]
  v)

The error message names the abstract variable that escapes:

open: existential type variable 'a' escapes its scope
(the body returns the bound value 'v' or an alias)

A worked example: Showable lists

A heterogeneous list of "things that can be shown" requires either an existential type or a shared concrete type. With existentials each element pairs the value with the witness for its Show instance, so a list of mixed concrete payloads can still be printed:

(defclass Show [a]
  (show [x] :cstr))

(definstance Show [int]
  (show [x] :cstr
    ```c
    char *buf = (char *)malloc(24);
    snprintf(buf, 24, "%lld", (long long)x);
    return (const char *)buf;
    ```))

(definstance Show [bool]
  (show [x] :cstr
    (if x "true" "false")))

(defn main [] :int
  (let [e1 (pack 42   (exists [a] [(Show a)] a))
        e2 (pack true (exists [a] [(Show a)] a))]
    (println (open e1 [a v] (.show v)))
    (println (open e2 [a v] (.show v))))
  0)

The pack/open sites stay inline; passing a constrained existential through a function parameter erases the constraint info and prevents open from extracting the boxed value (use the value at the construction site for now).

The stdlib/existential.tur helpers

The tur/existential stdlib module provides two convenience macros for the Show-constrained case. They are load-on-demand:

(load "stdlib/existential.tur")

(defn main [] :int
  (let [e (showable 42)]
    (println (show-it e)))
  0)
Macro Expands to
(showable x) (pack x (exists [a] [(Show a)] a))
(show-it e) (open e [a v] (.show v))

Show must be in scope at the call site, either via a local defclass or by loading stdlib/typeclass.tur. The helpers are macros so the existential type form appears literally at the pack/open site, which is required by the elaborator.

When to use existentials

What is not (yet) supported