Types

In short, types are mathematical systems, which is, at a minimum, is a set of value and a set of possible operations.

It may or may not form a closure with respect to these operations. The closure property is desirable and crucial.

Unlike mathematicians, we are also conserned with not just existence, but with representation and implemetation of our abstractions.

Out basic building blocks are interfaces and abstract dats-types.

“Data dominates”, so the algorighms, interfaces and implememtations follow the actual data-structures.

Data-types are ulitmate “cells” (building blocks) which have a “membrane” (an actual abstraction barrier) and “pumps and gates” (exported interfaces).

Data-types also have the inner structure (inside a membrane) which consist of a representations (an actual structuring) and corresponding implementation (based on the structure).

There could (and should) be more than one representation and implementation for the same abstract data-type (defined in terms of a formal specification of its exported interfaces).

At a higher level we have “type-classes”, “kinds of types” or more generally types of types. The most important is concept here is a Set of required interfaces (to be implemented).

This is known as “duck-typing” and, arguably, is the central notion.

So, a names sub-set of values, defined in terms of a set of possible operations and a [in]formal specifications for these operations. Plus the “type-classes” and “traits” and “modules”, which all are Sets of type-signatures.

Cardinality of a type

Cardinality (the size) is the only structural (general) property of a Set.

Associate a type with cardinality (just like of a Set) How many inhabitants (members) a type has. Ignore bottoms (they are relevant only in type-constraint solving)

data Void -- 0, no elements, just like The Empty Set

data () = () -- exactly 1, exactly this - no new information

data Bool = True | False -- just these 2. notice the |

data (,) a b = (,) a b -- a type-constructor, parametrized by a nd b

Shapes or forms

Notice that these types have distinct, unique shapes

| stands for an alternative or a possibility - OR ELSE (a “fork” - this or that).
, stands for AND ALSO (pretense in the same locality) (a “join” - this and that).

Notice that

only one “branch” of a “fork” can be taken (observed).
an aggregate (a compound) is fundamentally different (has its own unique /properties) from its individual parts.

Total

Knowing cardinalities of any two types (sets) we can know how many “arrows” (distinct relations or individual mappings) are there in total.

When we try to visualize (or formally define as a directed graph) the totality of all the possible relations we will notice that the resulting shapes (abstract structures) are the same (same number, same direction).

And this is it. This does not imply anything more than that - just similarity in its totality - a purely abstract notion.

The notion of duality based on cardinality alone is wrong and misleading.

Isomorphism

Any two types of the same cardinality could be viewed as isomorphic. This is a naive and too abstract to be useful assumption.

The shape (the form or structure) of the type is its distinct feature, out of which its properties arise (just as it is with molecules).

A “fork” is not isomorphic to a “join” in principle, but these are viewed by some sectarians as such.

Definition

The formal definition is this

there is a pair of total functions between two types (sets)
any composition of these two functions is an identity (a round trip)

When two types (sets) has the same cardinality, an one-to-one correspondence (a mapping between whole types) could be defined in principle as a pair of total functions (on whole types).

Ordering

As long as cardinality is greater than 1 a particular ordering has to be defined (become a part of an abstract mathematical structure).

An ordered set of arrows

Individual “arrows” (relations) between values has to be in a particular order.

Each “arrow” has to have a unique inverse “arrow” (which goes back where it started).

The meaning and validity of such functions does not concern mathematicians (only good philosophers).

Symmetries (rotations) could be formalized with such sets of functions.

n!

For any two types (sets) of the same cardinality \(n\) there are \(n!\) unique isomorphisms between them.

Same cardinality does not imply the same shape

Knowing that an isomorphism exists is enough. An isomorphism between types \(s\) and \(t\) is a proof that /for all intents and purposes, \(s\) and \(t\) are the same thing/.

This, of course, is bullshit.

The laws

The cardinality of a sum-type is the sum of the cardinalities of its constructors.

The cardinality of a product-type is the product of cardinalities of its parts.

It is said that these are duals, which is, again, bullshit.

The sum- and product- types have different shapes or forms.

Monoidial identities

() is a Monoidal Identity element for product-types (no new information). Void is an identity element for sum-types (Void has no members).

Exponentials

The type \(A \rightarrow B\) has cardinality \(B^{A}\) .

For every value of \(a\) in the domain, there is a \(b\) in \(B\). We can chose any value of \(B\) for every value in \(A\) so it is \(b \times b \times \dots \times b\) exactly \(a\) times.

Notes

Strings

A sequence of elements from the same set (an alphabet) is called a String and it is a “natural” type. A sequence of words from the same set (a shared vocabulary) is another one.

All Strings of length \(n\) denoted as \(S^{n}\) are \(S\times S \times S \times ... \times S\) taken \(n\) times.

Algebraic types

-> a set of all ordered pairs (arrows) - a function space { , } records are labeled Cartesian Products (a \(\times\)) { | } variants are labeled Disjoint Unions (an XOR) It is said that these two a “structural” dual to each other (all arrows being flipped).

Labeled means name-based selection (unordered in theory). There is always some particular order in an actual implementation.

Type-classes

Num a => [a] -> a This type states that for any type a of Numbers, sum is a function that maps a list of such numbers to a single such number.

Nesting

When we think of “structured values” we imply nesting of types.

Algebraic types can be nested, just as expressions.

Interfaces

Interfaces are as fundamental as cell membranes - they establish penetrable partitions.

Polymorphism

Parametric polymorphism is “on” types with the same nested structures. This is, of course, how different molecules with same parts can be used.

Sub-typing polymorphism is “on” types with same nested interfaces. This is “duck-typing” and the essence of message-passing (what goes in and when).

In general, abstracting out and formalizing some Universal mechanisms (found in reality) is the best strategy.

Sets of values

Types are based on a formally defined mathematical notion of a Set. Types are sets of values, defined by sets of constraints (corresponding to particual properties).

An optional set-subset relation for types is formally defined using the notion of type-class.

Constraints on type are of various kinds, most notably - structural (when values have a particular structure) and those defined by so-called duck-typing, which means to have a set of signatures to be implemented (to be an X is to exibit such and such behaviors), along with additional constraints, sometimes called “laws”, formally defined elsewhere.

The set-subset relation is used to specialize the resulting types or to define a family of types, using the formal notion of a type-class.

Type-classes

First of all, a type-class is a higer-level abstraction over types, and each particular instance of a type-class is type. The mathematical analogy is a Set of Sets while members (types) have an additional strucure (a set of required signatures).

Type-classes are defined by specifying a set of function signatures which are required to be implemented. Together all the signatures corresponds to a module singnature in ML or Ocaml. It is a closely related idea, but instead of being a Module an type-class is a type-level abstraction.

A class-constraint is modeled after a set-subset relation and implies that all the required signatures (for an instance of a particular type-class) are already implemented for a type.

Basically, a type-class defines a family of types using a set of required signatures together with an optional class-constraint.

Signatures act as “such that” selectors in mathematical logic.

It can be read as: “a subset of X, such that (list of specific constraints)” - which is very similar in its nature to declarative list comprehensions with generators and boolean guards.

Overloaded functions

This type signature implies that (+) is overloaded, which means could be applied to different types (provided both aguments are of the same type).

(+) :: Num a => a -> a -> a