Symmetry in type systems

Type systems exhibit a certain symmetry that causes almost all features to be duplicated. For example: sums & products, covariance & contravariance, unions & intersections, universals & existentials, exstensible records & extensible variants, etc. In each case you can transform one into the other with callbacks (continuation passing).

Even a function type like int -> string is made up of two parts. If we see a type annotation E(v : int -> string), that is saying two things: (1) the value v, when given an int, will produce a string (2) the continuation E will only call v with an int, and will be happy to get a string in return. The type annotation is not just constraining what the value can be, but also what the continuation can be.

What should I read to understand this two-sidedness better? Some question I have are: in physics when there is symmetry in a problem, it can often be eliminated to make the problem simpler. Can the symmetry in type systems be eliminated? For example you can imagine a purely CPS language where you have a type K(T) that represents a continuation that takes a T. Then you have K(A + B) = K(A) x K(B), and similar for other types. For function types you have A -> B = K(A x K(B)). K essentially flips the constraints around: the constraints that were laid on the value are now laid on the continuation and vice versa. Has this been explored? What should I read?

Another question is: does it make sense to separate the two pieces of a type? For example does it make sense to have a function type that only says "when given an int, v produces a string" but does not guarantee that the continuation will only call it with an int (perhaps in combination with other features like intersection and union)? Does this two-sidedness arise in other languages, like logic languages, where it's not so clear what are inputs and what are outputs?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Symmetry in logic, values and control, and type safety

The symmetry is already present, and maybe more apparent, in the logic that underlie the type systems. Logicians are fond of discussing whether all constructors should be defined, or only some of them with the others being macro-expressed through negations, whether negation is an operation or a meta-operation using De Morgan's formulas, whether calculi should be two-sided (representing input/hypothesis and output/results) or one-sided (mixing everything, as in linear logic), etc. They also have more axis for symmetry, such as polarization, which *may* correspond to a local, typed-directed choice between strict and lazy evaluation. I think if you want to read more about those symmetries, you should look at what logicians write on the topic (keywords "linear logic", "bureaucracy"; I would look at work by Dale Miller, but have no exact reference).

In my humble opinion, it is not obviously right (and possibly wrong) to consider that sums are useless when you have product and continuations, for example. The following is highly informal. I think there is a difference between values and control, and indeed eliminating a sum value gives a control product, but the link between a control product and a value product (eg. encoding continuations as functional values and then control product as a product functions) is semantics-preserving but maybe not the identity, and in particular it is not performance-preserving in practice. I have tried to consider this issue in the discussion of the Multi-Return Function Call work, but am unsure what is happening.

Finally, I do not buy your idea that a type annotation constrains both the value and its environment. You say that `E(v : foo)` says both that v respects the invariant corresponding to the type `foo`, and that the environment `E` assumes no more than `foo` on the value it consumes. But I think this latter guarantee is rather the result of a global type safety result: someone has done the meta-theoretical work to prove that all expressible contexts respect type-safety of the annotated value. So it seems a bit strange to claim that this safety is a property "of the type annotation" in isolation, when it relies on a system-wide claim that may not hold in practice. On the contrary, the link between the correctness of the annotation (v : foo) and the behavior of v can (in an fully explicitly typed system) be established by considering `v` and `foo` in isolation.

Thanks for your answer. I

Thanks for your answer. I will consider it in more depth but here I just explain why I said that the type annotation constrains the environment. Consider a language like C#. If you have a v of type Car, and then do E(v : Vehicle) then the environment is constrained by the type annotation: it can only assume that v is a Vehicle. On the other hand, the value is *not* constrained by the type annotation, because a Car is already a Vehicle. Does this make sense?

I think the correct reading

I think the correct reading of this is that, if you consider `(v : Vehicle)` as a term (in my previous answer I assumed it was some kind of meta-notation to say E(v) with an independent judgement that (v : foo) holds), it is a value of type `Vehicle`, whereas `v` was of type `Car`. `(v : foo)` is a coercion.

Value and environments

Replying to myself:

On the contrary, the link between the correctness of the annotation (v : foo) and the behavior of v can (in an fully explicitly typed system) be established by considering `v` and `foo` in isolation.

While I still think this is true, I must note that the formulation may be a bit misleading. The typing judgement `v : foo` establishes invariants (properties, "contract"...) on `v` alone, but, as soon as `v` contains higher-order types (that is, negations), this invariant will also speak about the environment. For example if `foo` is `(int -> int) -> int`, saying that foo is well-typed implies that it returns an int value if passed a value from the environment that itself behaves well.

I'm unsure whether this what Jules was speaking of, or if he was having a different kind of "constraints on the environment" in mind.

That is exactly what I was

That is exactly what I was speaking of, but it is not restricted to higher order functions. Another example is ADTs: if you say v : exists T. [...] then that puts the constraint on the environment that it cannot use T components of v except via the ADT.

This even goes for simple types like int & Car & Vehicle, depending on your point of view. If you say (v : int) then that constrains the environment to be an expression that does not call e.g. reverse on v. What I mean is that if you have E(v : int) then the environment could be rejected regardless of what v is. Similarly, v could be rejected regardless of what E is. The correctness of the whole annotation E(v : foo) depends on both parts. This is also related to contracts: if you have a contract foo and you do E(v : foo) then foo will blame v for some errors but it will blame E for other errors.

sums & products

Nice: relevant, a references and discussion of the previous work

That is an excellent reference indeed for Jules question. From the title alone, I expected to find a discussion of esoteric type systems for reversible or quantum computations, that I personally quite boring. In fact the focus of the article is more general and quite relevant to the present discussion.

It also mentions the bibliography on logic and continuations that I was thinking of (but didn't not a good point of entry for). In other words, very well put.

(Regarding other branches of work that discuss the duality of values and contexts, I suggest looking at the work in Game Semantics for lambda-calculi, and realizability.)

Thanks! That looks very

Thanks! That looks very interesting. I'm afraid I don't really understand it however, I guess I will look at the references first :)

Duality of computation

The canonical references are probably Filinski (MSc thesis 1989, there also is a paper, but it's behind a paywall), Curien & Herbelin (ICFP 2000), and perhaps Wadler (ICFP 2003).

PS: Note that this is not so much a question of types as it is a question of computational primitives. Types primarily help shedding light on what's going on.

Thanks. I have not finished

Thanks. I have not finished reading them but what I've read so far is quite nice.

One specific question that I have is regarding union/intersection types, which doesn't seem to be addressed in those papers so I'll ask it here. We can characterize some types by the set of values they are a valid type for. For example int and set(int) = {... -1, 0, 1, 2 ...}. The same goes for function types: set(A -> B) = set(A) -> set(B), where A -> B on sets constructs a set of all the functions from set A to set B (some will not be computable of course). For union types the natural thing is set(A union B) = set(A) union set(B) and similarly for intersection. But now something goes wrong if you add contexts: K(A intersect B) != K(A) union K(B). To see this take for example A = int -> int, B = string -> string. Now K(A intersect B) includes the context that calls its argument on 3 and then calls its argument on "foo". But this context is neither in set(K(A)) nor in set(K(B)). But what you can do with a K(A intersect B) is the same as what you can do with a K(A) union K(B), namely applying it to something that is both an A and a B zero or more times. In other words K(K(A intersect B)) = K(K(A) union K(B)). So either the set notion has to give or the duality between union and intersect has to give. On the other hand the rule K(A union B) = K(A) intersect K(B) seems quite valid regardless, but probably fails again if you wrap both sides in K. This also implies K(K(A)) != A. That seems OK but how to resolve this asymmetry between union and intersect?

Look over there...

Types-as-sets a bit too naive

It is a bit too naive to expect to give easily a semantics of types as set of terms and contexts operating on them. It can be done for some sufficiently well-behaved languages, but you will have/need some additional structure. For example, the set of contexts that could be denoted by K(T) for some T needs to be closed over some reasonable operations (of compositional construction of contexts from other contexts). For example if you have tuples/products in your language and K1, K2 are contexts, (\x -> (K1[x],K2[x])) also is a context. If you want a "set of contexts" to represent the "contexts at type T", it must be closed by this product operation.

But direct set-theoretic operations such as union will not necessarily preserve closure by those operators. So you don't take the union of those set-of-contexts-at-some-type, and expect to get a set-of-contexts-at-some-type; you take the closure of this union by these operations of interest. And generally this closure coincides with a form of double-negation, so indeed it makes sense to define K(A intersect B) as K(K(K(A) union K(B))) -- which is not too painful with proper notations.

You should look into the literature of realizability, which discusses those things in depth. I don't know what would be a good introductory reference, as most of the material is aimed at logicians rather than programming language people, but with your Curry-Howard glasses on you should be able to make sense of (the beginning of) Specifying Peirce's law in classical realizability, by Mauricio Guillermo and Alexandre Miquel, 2011.

free associations

Jules Jacobs : What should I read to understand this two-sidedness better?

Not sure ... really interesting questions, though. If you're in a mode to gather clues very widely -- then sort wheat from chaff after -- perhaps you won't mind low grade suggestions near lunatic fringe in quality. (Sometimes a lot of hypotheses are better, to avoid being steered by confirmation bias.)

Something about the continuation aspect (some now, some later) makes me think of boundary logic: lookup G. Spencer-Brown, Bricken, Shoup, and Kauffman. Criticisms of Spencer-Brown include 1) sounds like bunk; 2) too abstract to be useful; and 3) but that's equivalent to boolean algebra.

The rest of this is personal anecdote. I never cared for abstract algebra, but around 1981 I started looking for the highest meta level explanations I could find about why things fell into the taxonomic groupings they did. In math that led to category theory, which was really unsatisfying, since it seemed little more than naming broad patterns (probably because I didn't get it). But related to the above, arrows can be about crossing boundaries, since otherwise nothing distinguishes source and destination.

Free associating further, something about distinguishing figure and ground in art might be useful in thinking about duality with a context spin. That's all I have.


First, I would extend Rys' observation about category theory by suggesting that category theory alone is indeed an extremely sparse framework within which to operate. The computational view of category theory that's best known is probably Eugenio Moggi's, and the most-likely-pertinent type-theoretic view is probably Categories for Types. Be warned that the latter is certainly not an introductory text.

To the extent that the duality you observe is reflected in the distinction between Constructive and Classical logic (presence or absence of the Law of the Excluded Middle, double-negation elimination as an axiom, etc.) you might find A Formulae-as-Types Notion of Control interesting. The concrete relevance of this work is reflected in the classical extraction module for Coq, which "enriches the Coq proof assistant (version 8.2 or higher) with a set of commands to extract programs from classical proofs built in the Coq environment," vs. the built-in support for extracting programs from constructive proofs. But here I am making a pretty large set of assumptions about the extent to which the constructive/classical divide is representative of (isomorphic to?) what you mean with respect to the duality you observe.