– 0: Nat and incr: Nat => Nat for natural numbers,

– empty: List[Any] and cons[T](head: T, tail: List[T]): List[T] for lists.

– Lambda-abstractions for functions.

Sematically, contents of a datatype is defined to be a least fixed point of what can be constructed by a finite tree of constructors.

To embrace the open world, you need codata. Codata isn't defined, it's

*described*by defining a type class. Codata types are described by their consumers (others prefere “destructors” or “structors” to underline the duality with constructors). Consumers are maps transforming objects of a particular codata types into objects which might be both data or codata. Codata cannot be constructed within the language, it can be only

*processed*. In other words, codata types describe entities foreign to the mathematical world. In programming, this would be the user input and message feeds from foreign systems. We know how to consume, i.e. process them, but they are inherently external. When describing the physical world, these are quantities and spaces, media, interactions, etc. Say, a measurable quantity of type T could be described by a consumer measure: Quantity[T] => T. All first order theories like groups and algebras can be described as algebraic codatatypes and non-first-order ones like topological spaces as generalized codata types.

Functions consuming codata objects are necessarily type-polymorphic (accepting all types of the given codata typeclass). Note that one cannot do anything with a codata except through its consumers, which reminds of abstract types and encapsulation in object oriented programming. This analogy is not incidental: codata can be modelled by data. We can give an explicit example of Feed[T] by providing a List[T], we can provide lots of explicit examples of concrete groups and so on. The language providing a good modelling facilites should provide a casting operator for construction of a codata instance by providing a model: implementation of codata type and its structors by a datatype collection of functions on it. Once casted (or “blessed” in Perl'esque paralence) to codata, the object cannot be “uncast” back to it's representation. My speculation is that provided such an operator, there is no need in type polymorphism and type classes except for natural codata type classes and type class polymorphism.

The ability to describe codata types and incorporate them into the type system is essential to describe nature and/or take account of interactions with foreign systems cleanly. (Like it's done for example in the Charity programming language.) I'm absolutely sure that the development of a Dependent Object Type Theory extending Observable Type Theory or its cousin by proper handling of codata is a major programme in the context of functional programming.

Physical concepts (beginning with the real line and eucledian space) cannot be modelled well in constructive universe, which is the main reason why mathematics makes use of “ideal” (in sense of "imaginary", not "perfect") operations: operations which cannot be carried out constructively, but can be thought of. The weakest of such operations is the construction of a power set, a set of all subsets of a non-finite set. It's absolutely necessary for the construction of a model of a real line, and allows representing all functions between sets (instead of only computable ones). Stronger nonconstructive techniques (all of which are essentially forms of the axiom of choice) lead to stronger paradoxes. Well, the ideal world doesn't work as straightforward as one would naïvely expect, but there is a strong confidence that it's well-founded and consistent based on the fact that the world somehow works.