wiki:Types

Types

We, humans, it is said, are capable of thinking categorically. At least some of us.

Categories (or kinds or sorts of things), however, like Numbers, are merely constructions of the mind (of an external observer) -- generalization of a heap and, like Numbers does not exist outside your head.

"What kind" is hardwired deeply in the mind of an observer (capable of using abstract categories) and hence it is at the core of a language. Some nouns stands for a kind of things - a dog, a man (while adjectives stand for what attributes or qualities a thing has).

Kinds and classes are synonyms. It is just words from different cultures to refer to the same abstraction - a category - generalization of a heap.

Simple (naive) classes or categories are like heaps (or buckets) for sorting things. Each thing goes into a particular bucket - this is this, this is that. The whole process is called the "bucket sort". Mail and parcels are sorted this way.

Advanced (subtle) categories are made out of behavioral traits - this is capable of this, this could do that. They are adj verbs.

Every human language has them (reflecting actual reality or what is). In English they usually have the suffix "able" - Foldable, Comparable, etc.

Abstract concepts

Abstractions may (or may not) have a Structure and/or Behavior.

They could be simply

  • IS A - classes of things values (kinds)
    We often say that v has type T or, interchangeably, that v is a T (note that "is a").

Tom is a cat, Porsche is a car.

  • WHAT IT TAKES TO BE AN - behaviors (traits)
    The definition of a class defines what it take to be T. Each instance v of T is indeed a T.

Type-classes define (by specifying interfaces to be implemented) behaviors - what it takes to be an... (contrary to simple "is a").

Specialization

Concepts form abstract categories which could be specialized by adding more specific constraints (structural or behavioral).

It is an operation similar to defining a subset of a set using some predicate. To filter out some subset.

Generalization

Abstract categories could be even more generalized by removing or relaxing certain conditions (constraints).

To generalize is to establish a common superset to which given sets are specializations (upon some criteria or constraint).

In math

A simple class (which is literally a simple type) is a naive category. A heap.

A Set is an abstraction (a rigorous model) of a class of values - a formalized generalized heap (or the most basic collection), if you will. It has only notions of membership (is it in or not) and of a count (how many items it has).

A simple class is a type (literally a named set of values).

Sum-type (an Enumeration)

An enumeration is the simplest set of values - this and that. It could be of size 1 or even empty (of size 0).

Such a type is traditionally called a sum-type, because it behaves like a sum. Sort of.

This OR That (an Alternative)

A set of values could be partitioned into a subsets (of non-zero size). Each subset of a set is logically distinct (separated by an abstract partition) from the others.

An alternative is either of this or that it is (or more correctly - could be viewed as) an enumeration - a sum-type.

In the new Scala that would be:

type Command = "Click" | "Drag" | "KeyPress"

which is literally says it all - this type is either of three separated (partitioned) by | strings.

And then you will pattern-match on a value of this type.

This AND That (a Product-Type)

A combination (of two or more sets) is a product-type - a union of two sets. It behaves like a Cartesian Product - all combinations (not permutations) of given two (or more) sets.

A product with an empty set is an identity operation.

In programming

I absolutely love this quote and am reproducing it here verbatim In functional programming the universe of values is partitioned into organized collections, called types.

I would rather s/collections/sections/ or just s/organized// s/collections/sets/ but the original quote is beautiful one nevertheless.

The notion of a Type is central

Types rigorously separate out concepts. Types partition The Universe Of Ideas into well-defined subsets. (hate this bullshit, but the metaphor is good). Just this.

With types we partition a whole program into an semi-independent (orthogonal) parts or concepts, so they could have been developed semi-independently.

Implementation side

A type defines both the structure of a data element and the set of operations that are possible on those data.

To be an Xxxx is to have this shape and to implement (to be able to do) this and that.

USE THE MOST SPECIFIC TYPE (the smallest set of values).

We use Interfaces (named sets of type signatures, preferably statically checked) to communicate across partitions (preserving abstraction boundaries).

A type defines a named set of possible values complemented with a set of possible operations on values (a set of interfaces). It defines a category of values (or objects) and behavioral traits which are common to all of the objects in this category. Just this.

Type-Tags of Lisps

Types tag (label) a universe of values into formalized, well-defined abstract categories, if you will.

Types are tags, attached to expressions or values to indicate what kind of value it is (to which set it belongs - may be more than one). Just this.

It is good to think that there is a separate environment in which each value has a tag associated with it. It is sometimes called the static environment, as opposed to dynamic environments used to carry on (implement) the process of evaluation.


Typing is a process of defining a set of constraints (also called laws or contracts) for a distinct set of values.

A type is defined as a set of possible operations on values. Implementation details may constitute additional constraints.

A type is referenced by a symbol.

Technically tying is a discipline of associating values in some dynamic environment with a type information in a separate so-called static environment.

The crucial thing is to have a strong typing, which essentially means that every value has a type and there is no implicit coercions between values of different types. Common Lisp is a strongly-typed language.

Basically, we have a two separate environments with two separate languages (DSL for types and general purpose for the code).

The purpose of typing is to define a set of restrictions (a specialization), name it and then check the constraints (enforce the contracts) at a compile time.

There are so-called machine type (or concrete types) such as int or float, which reflects how the data is actually represented within a machine, and abstract data types (interfaces) on top of these.

Mixing types and code, like it is in Java, is a form of verbose idiotism. Segregating type information in a DSL a-la Haskell (or to some extent in Scala) is the right way. Go has been evolved a remarkably lightweight static type system.

BTW, Java is a monument (a colossus) if applied packer's mindset.

Complex abstract (interface) types could be parametrized with a type parameters to yield a specialized (constrained) type, such as []string or List[Int].

So-called type constructors (expressions which define a specific type) could be used in pattern-matching expressions for explicit destructuring.

append [] ys   = ys
append (x:xs)  = x : append xs ys 
def eval(e: Expr): Int = e match {
    case Number(n) => n
    case Plus(x, y) => eval(x) + eval(y)
}

Another purpose of types is to define a behavior via an Abstract Data Types, which is basically a set of interface types together with a set of rules which must be followed by an implementation.

This idea is augmented the notion of Duck Typing provides a general mechanism of substitution (and grouping and chaining) by behavioral traits.

The Python is a champion of abstracting out behaviors. It defines, for example, what it takes to be an iterable, to have a total ordering, or even to be a collection.

from functools import total_ordering

@total_ordering
class User():
...
    def __eq__(self, other):
        if type(other) is type(self):
            return self.id == other.id
        else:
            return False

    def __lt__(self, other):
        if type(other) is type(self):
            return self.name.lower() < other.name.lower()
        else:
            return NotImplemented

Notice that equality is defined in terms of an id while sorting is done by the name

Last modified 6 months ago Last modified on Sep 25, 2019, 5:55:55 AM
Note: See TracWiki for help on using the wiki.