October 20, 2016

Speaker: Yishuai Li

Progress reports due Tuesday

Questions

How to comprehend the value of a all(t.\tau) type? Is it just a function from t to e which is typed \tau?

[SCW: That is one way to look at it. However, note that this function must be parametric. It cannot use the type argument.]
Impredicativity seems like a dangerous thing that opens up possible inconsistencies, e.g. Russell's and Girard's paradox. How does one know when it's safe to add impredicativity to a type system, and how should we even think about such a type system denotationally?

[SCW: Good question. Some type theorists disavow impredicativity as too dangerous. Proofs that impredicativity is consistent usually rely on some sort of impredicativity in the meta-logic reasoning itself. ]
Is there a connection between the polymorphic types described in this chapter and the polynomial types described in Ch.14?

How to prove regularity in the type application case App ?

[SCW: perhaps you are picking up on the fact that Lemma 16.1 depends on Lemma 16.2? We need to use substitution to show regularity in the App case.]

Is there any way to show the encodings in Section 16.2.1 work (and are in a sense faithful), without appealing to parametricity? The encoding for unit relies on the fact that the identity function is the only function Vr. -> r, which seems difficult to show without parametricity arguments. Of course if we didn't care about our translation being faithful we could have translated unit to anything we wanted.

[SCW: No. We need parametricity for this reasoning. See http://homepages.inf.ed.ac.uk/wadler/papers/gr2/gr2.pdf]
I think of this chapter as the generalization of things that we were doing till now. The ad hoc sum, product, natural number types have been defined just from function types at the type and term levels. What we thought of as isolated things find their place in the spectrum of things. The big achievement, I believe, is the parametricity theorem, which says something fundamental about the nature of types themselves. The book shows how it works, but is there a proof of the parametricity theorem given somewhere?

[SCW: we'll get to the proof of parametricity in Ch. 48]

Does the parametricity theorem similarly apply to rank-restricted fragments, so that we also just get "theorems for free"?

[SCW: I believe so.]
How would the “free theorems” be useful in practice?

[SCW: reasoning about the correctness of optimizations, for example]
I am not clear about the proof of i: forall(t.t->t) being polymorphic identity function. Why should we use property to prove that?
Bob Harper really emphasizes the power of parametricity to reason about functions. Like,
```
  f :: forall a. a -> a
```
can only ever be implemented as the identity function. I fail to see what we gain from this example. How is this useful for this example? Or if it's not, what are some examples where this property is actually useful?

[See also: Robert Atkey. From Parametricity to Conservation Laws, via Noether's Theorem]
I feel like the discussion about parametricity in Section 16.3 glosses over most of the main difficulties of the proof. I know we're going to discuss this later in the semester, but can you state at a high level how to show that any function: i : Vt. t-> t enjoys the property that forall t, P : t -> Prop, P x -> P (i[t] x)?

[SCW: patience....]

The rank of a type appears to be counting the complexity of the type in terms of quantification and arrows. Why is this important? Are there results that actually say something about these ranked types, e.g. decidability? Also, negative occurrences always seems to be complicating things, e.g. because of contravariance - is this related?

[SCW: Type inference for System F is undecidable, but Rank 2 polymorphism is decidable (as is Rank 1, i.e. the Hindley Milner system).]
At the end of the book, Bob gave a definition of "iter" based on church encodings of natural numbers, but the book also has comments on how System F is still one step away from being able to evaluate itself.

Is the missing element general recursion? Why is it not derivable in system F? Is the fixpoint operator not typeable in system F? In haskell, by virtue of lazy evaluation, we can define something like fix f = f (fix f), which has type (a -> a) -> a, can we not do the same thing in System F if we introduced lazy evalution?

[SCW: See: Matt Brown, Jens Palsberg: Breaking through the normalization barrier: a self-interpreter for f-omega. POPL 2016].