October 14th, 2008

beartato phd

(no subject)

I am 28 today. I received surprise cookies in the shape of alarmingly cute wugs. Some people sure have my number.

Bob's class yesterday mentioned that System F's termination is intimately bound up with the fact that it is parametric. I found a paper that Bob wrote in the late 90s that gives the gory details in an easy to digest form: Parametricity and variants of Girard's J operator.

The punchline is that if you have a operation that can tell whether two types are equal and do different things accordingly, say
G |- M : σ     G |- N : τ
--------------------------------------------
G |- if σ = τ then M else N : τ

(notice the cute asymmetry that the if-then-else can have type tau no matter what, since if it comes out N, then it has type tau, and if it comes out M, then, well, sigma equals tau, so it also has type tau) then you can write a nonterminating term
X [σ] X
where
X : IdType = Λα.λx:α.if &alpha = IdType then x [IdType] x else x
IdType = ∀α.α→α