UP | HOME

Understanding types

Every value has a type, which means, conceptually, that it belongs to a particular Set.

The Set could be formed as a results of a constraint satisfaction process, which corresponds to multiple union/intersection operations.

Duck-typing (based on “traits” or required interfaces) is the way to define a such a set of constraints (at an interfaces level).

It is remarkable that all the types could be either so-called

This has very deep correspondence with what we might loosely call “the structure of reality”, and with the 3 fundamental sequencing flow-chart patterns – composition, branching and recursion (looping).

Product types capture the universal notion of having a structure (and-also in human language).

Sum types capture the universal notion of a possible outcome (or else in human languages).

Function types capture the universal notion of a transition in a single step (implication, transformation, transition, which implies a direction) – an arrow in a human symbolism.

This means that types are not merely Sets of values, but a whole “systems” with associated Set of possible operations (on values) and informally defined constraints.

This gives us

OO has lots of complications related to the notion of an “inheritance”, which means to define a proper “is a” relations, respecting all the “logical” constraints.

Better language just compose (as a “product”) individual “traits”, which is not necessarily nesting (a set-subset relation).

This is the fundamental issue – traits or “behaviors” do not have to be a proper Subset. Everything follows from this.

There could be some arbitrary nesting (Subsets) of interfaces but it is not strictly required. This relaxation solves the fundamental problem of “too rigid classifications”.

Again, just “circles” full of individual values. We defines these “circles” (Sets) in terms of possible operations.

This is exactly how we define, say, a Semigroup in an abstract algebra.

We may add additional constraints, such as particular relations among elements, and we would get a Monoid or even a Group.

The notion of a type-class (as by Wadler) is how we define as a common Subset of required operations (implemented interfaces).

This is exactly the same notion which is behind the Liskov Substitution Principle (idicating that it is a universal) - it is the set-subset relation at the level of type-signatures (interfaces).

If something implements (walks like a duck), it can be “substituted” (the methods can be called on a reference of distinct supertype).

One more time - as long as we define the types (Sets of values) in terms of operations (abstract type-signatures and interfaces), and then select a common Subset of the these operations (type-signatures, interfaces) we are all set.

The additional informally stated constraints, invariants, and “laws” cannot be expressed with this “set-and-logic” classic conceptual framework.

Nothing, however, prevents one to add one more component to the conceptual closure (a product) already which has a Set of Operations. It couls be a Set of Constraints, even with “lambdas” (lexical closures) that check them.

But fundamentally, it is still “sets, subsets (nesting), products, graphs and logic”.

Author: <schiptsov@gmail.com>

Email: lngnmn2@yahoo.com

Created: 2023-08-08 Tue 18:39

Emacs 29.1.50 (Org mode 9.7-pre)