heterogeneous polymophic structures in SML (delaying type-checking to run-time)

I'm sure this is well known to those who know, but I keep meeting people who don't know...

Heterogeneous lists, and other such dynamically polymorphic data structures, can be written in Standard ML by pushing type-checking to run-time using exceptions. Here's a little example:

(* exceptions that wrap up some data *)
exception StringExpWrapper of string;
exception IntExpWrapper of int;

(* generic kind of data: an informal name for the data and the
   exception that holds the data *)
datatype generic_data =
  GenericData of { kindstr : string, dataexn : exn };

(* helper function to wrap up data in exceptions and give them a kind string *)
fun wrap_int i =
    GenericData { kindstr = "int", dataexn = IntExpWrapper i };
fun wrap_string s =
    GenericData { kindstr = "string", dataexn = StringExpWrapper s };
fun wrap_generic ex =
    GenericData { kindstr = "generic", dataexn = ex };

(* To try and pull integer from generic data; will raise the wrapped
   exception if the kind-string is "int" but the exception is not the
   IntExpWrapper. *)
fun unwrap_int (GenericData { kindstr = "int", dataexn }) =
    ((raise dataexn) handle IntExpWrapper x => SOME x)
  | unwrap_int _ = NONE;

(* empty list *)
val empty_list = []  :  generic_data list;
val list1 = [wrap_string "foo", wrap_int 12, wrap_int 3];

(* we can sum the integers in a generic list... *)
fun sum_ints l =
    List.foldr
      (fn (data,count) =>
       case unwrap_int data of SOME n => count + n | NONE => count)
      0 l;

(* a little test to sum of our first generic/heterogeneous list *)
val sum1 = sum_ints list1;

(* we can create new kinds of exception for new type of data we want
   to wrap up and add to our list ... *)
exception SomeNewDataExn of int list;

(* now we can extend our old list with elements, even those of the
   new type *)
val list2 = [wrap_int 2, wrap_generic (SomeNewDataExn [1,2])] @ list1;

(* and we can apply the sum function again to this new list... *)
val sum2 = sum_ints list2;

More generally,  exceptions give one the opportunity to delay type-checking until run-time. Generally this introduces the opportunity for a programming error to cause a run-time exception. However, by a little careful wrapping of things in functors, you can keep it type-safe, and allow dynamically extended the kinds of data available during execution time. See for example Isabelle's universal type, or isaplib's generic polymorphic tables.