Lambda the Ultimate

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 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.

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 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.

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 interesting. I'm afraid I don't really understand it however, I guess I will look at the references first :)

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?

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.

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.