If dynamically typed languages are truly statically typed, unityped languages, what is the (finite) type expression of the one type?

Question

Some claim that dynamically typed languages are in reality statically typed, unityped languages. This would imply to me that this one type should be expressible as a static, finite type expression, so can anyone provide such an expression? You can make whatever assumptions you need to make about the base types in the language, but please make sure the language would support types of unbounded size, e.g., lists, recursive types. It would also be nice if it supported records and variants, but whatever helps to illustrate the point will work. I'm also assuming that the language will be required to support some form of sum type, right?

Answer 1

This is entirely dependent on the language, and even on the implementation. The type would typically include entries for primitive functions, external library bindings (e.g. file handles), byte-compiled functions, etc. in addition to the data types of the language.

You can see a type like this in an interpreter for a dynamically-typed language written in a statically-typed language.

Here's an example of a type that's sufficient for a Logo value, showing that you don't need much to get started. Logo's values have a very simple structure: the only primitive type is the string, and the only structured type is the list. I use OCaml notation for the type.

 type logo_value =
   | Scalar of string
   | List of logo_value list

For example the logo value [3 [4 5]] is represented by the OCaml value List [Scalar "3"; List [Scalar "4"; Scala "5"]]

Here's an example of a type for an interpreter for a fragment of Scheme, again written in OCaml notation. Scheme is a larger language, with a range of primitive and structured types, functions as first-class values, and input/output objects.

type scheme_value =
  | Boolean of bool                (* #f, #t *)
  | Exact of Num.num               (* integers and rational numbers *)
  | Inexact of Complex.t           (* reals and complex numbers *)
  | Char of int                    (* Unicode characters *)
  | String of string               (* Strings (mutable, fixed-size) *)
  | Symbol of string               (* Symbols (immutable) *)
  | Cons of scheme_cons            (* Pair (mutable) *)
  | Vector of scheme_value array   (* Vectors (mutable, fixed-size) *)
  | Primitive of scheme_value list -> scheme_value   (* Primitive function *)
  | Lambda of string list * scheme_value             (* (argument names, body forms) *)
  | Port_in of in_channel          (* I/O port (input) *)
  | Port_out of out_channel        (* I/O port (output) *)
  | Eof                            (* (eof-object) *)
 and scheme_cons = {mutable car : scheme_value; mutable cdr : scheme_value}

Answer 2

Here is how Dana Scott and Christopher Strachey would have written the unique type. They called it a "domain".

$$ D = {\bf 1} + {\it Int} + {\it Bool} + {\it Char} + (D \times D) + (D \to D)$$

• The 1 is a singleton type, that of nil or null whatever.
• Int - for integers
• Bool - for booleans
• Char - for characters
• $D \times D$ - for pairs of values
• $D \to D$ - for functions over values

We often call such a type a universal domain. It contains everything!

If you want lists, for example, just pick the subset represented by the equation

$$ L = {\bf 1} + (D \times L) $$