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?


2 Answers 2


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}

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) $$

  • $\begingroup$ Not knowing much about domains, I wonder: is it really okay to gloss over the cardinality issues that arise from having functions in your domain? Without further nuance, this implies that $D^D \subseteq D$, which is impossible by cardinality. $\endgroup$
    – Alex R
    Commented Mar 6, 2016 at 17:52
  • $\begingroup$ @AlexR In type theory, it's common to say “function” to mean “computable function” or “computable partial function” (depending on the context). In theory of computation this is an important consideration and needs to be explicit, but in type theory we're usually not interested in non-computable functions at all and tend to exclude them implicitly. $\endgroup$ Commented Oct 30, 2019 at 15:33
  • $\begingroup$ In domain theory $D^D \subseteq D$ is quite possible and normal. To be precise, "domain" here means a countably-based $\omega$-algebraic bounded-complete partial order. There are other kinds of domains of course, with similar properties. $\endgroup$
    – Uday Reddy
    Commented Mar 11, 2020 at 14:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.