Jason (jcreed) wrote,

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
X : IdType = Λα.λx:α.if &alpha = IdType then x [IdType] x else x
IdType = ∀α.α→α
Tags: birthday, math

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded