View Source Document

Chris Pressey.md

Commentary by Chris Pressey

This work is distributed under a CC-BY-ND-4.0 license, with the following explicit exception: the ratings may be freely used for any purpose with no limitations.

Type Systems

Counterexamples in Type Systems

.

Should Your Specification Language Be Typed?

If you've been raised on languages like Coq and Agda you might even be suprised to learn that specification languages needn't be typed at all.

On Understanding Data Abstraction, Revisited

Cogently shows that there is a difference between abstract data types and object-orientation, and describes it.

In Search of Types

When a type theorist says "type" they mean something from the typed lambda calculus. When a software engineer says "type" they mean something they use to stop some bits of their data from being confused with other bits of their data. When the two groups meet, hilarity ensues.

Several types of types in programming languages

A pretty short paper about how the concept of "type" historically came about; complements [In Search of Types][] that way. In particular noting that the parallel evolution of "type" is not too surprising, because for computer scientists it was motivated by very practical concerns (of memory allocation and avoiding errors), while for logicians it was motivated by very abstract concerns (of avoiding logical inconsistency). Gives the following contrast as an example to emphasize this: well-typed terms ensures normalization, however there are well-typed programs that do not terminate.

(This makes Haskell's choice, to basically take a type theory and remove the normalizing property so that one can "write real programs in it", seem a bit bizarre to me. Well, it already seemed a bit bizarre to me, but this puts yet more context arount it.)

Unfolding Abstract Datatypes

So the basic idea is that ADTs can be seen as corecursive data types, which can be unfolded into infinite structures, which can then be reasoned about with the usual style of equational reasoning familiar to functional programmers.

I should read it over again and take more notes. But here's a quote:

Two instances of an abstract datatype are clearly different if there is an experiment — that is, a sequence of operations provided by the signature — yielding distinguishable concrete outputs (...) and conversely, if no such experiment exists, we consider the two instances to be equal.

Compare this to "Final algebra semantics" from algebraic specification, for example "SE 507 Algebraic Specifications".

See also "Fast and Loose Reasoning is Morally Correct".

Initial Algebra Semantics is Enough!

Apparently initial algebra semantics were thought insufficient for nested types and maybe other things. This paper apparently shows they're not.

Nested types: the subtle different between "family of inductive types" and "inductive family of types". "Perfect trees" given as an example; instead of a branch node being a pair of Trees, it is a tree of pairs. The "other type" appears "inside" the induction, complicating things.

But there is a generic construction that works even for this nested situation. For any category C, there is a category of endofunctors on C, where objects are functors and morphisms are natural transformations. By instantiating (lifting?) the generic fold and build functions on this category of endofunctors, you get something generic enough to work across an inductive family of types.

Of course, now the structure map of an algebra is a natural transformation, and the result of a fold is a natural transformation from a nested type to the carrier of the algebra.

I can kind of see it. I'm content with that.

Type and Effect Systems

.

Abstract Types have Existential Type

.

A Theory of Type Polymorphism in Programming

.

type safety - What is the difference between a strongly typed language and a statically typed language? - Stack Overflow

.

What is a strictly typed language? - Stack Overflow

.

Coeffects: The next big programming challenge - Tomas Petricek

.

Type Constraints · The Programming Languages Laboratory

.

The algebra (and calculus!) of algebraic data types

.

What is a type and effect system? - Stack Overflow

.