Advanced Topics in Programming Languages Series:...

Google Tech Talks
April 18, 2007

ABSTRACT

Advanced Topics in Programming Languages Series: Parametric Polymorphism and the Girard-Reynolds Isomorphism. This talk is based on a series of papers by Philip Wadler, a principal designer of the Haskell programming language. Featured are a number of double-barreled names in computer science:

* Hindley-Milner (Strong typing without having to type the types)
* Wadler-Blott (Making ad-hoc polymorphism less ad-hoc with parametricity)
* Curry-Howard (Isomorphism between types and theorems, terms and proofs)
* Girard-Reynolds (Isomorphism between types and terms in the presence of parametricity)

The talk will conclude with a programming technique...

• Category

  Howto & Style

[twifkak]

I thought it was pretty good. I got lost for a bit on P2 & F2, but I found the explanation of Curry-Howard to be the best I've seen.

[John Sowa]

It's a good overview, but the opening section about Frege and Russell is incomplete and irrelevant. C. S. Peirce invented the algebraic notation for predicate calculus, which Peano modified and Russell adopted. Furthermore, Peirce had published an article on "Logical Machines" as early as 1887, in which he discussed mechanical theorem provers as well as Babbage's machines. Russell's version of types is totally different from the later types that have applications to programming languages.

[shatakan]

The opening section about Frege and Russell is incomplete...

...and inconsistent.

[Bounce0Up0Nessa3]

Oh, I'm in This part of youtube Again....

Was just looking for repeat episodes of the big bang theory....

[tohopes]

I'm thinking "more semantic meaning" in terms of structural typing or type classes as someone brought up in the q&a at the end.

[tohopes]

Presented examples of "code inference" seem useless. The technique would become more valuable technique as you put more semantic meaning into your type hierarchies (coding theorems as types as he suggests earlier on). But then at the end he suggests that the whole inference thing falls apart without pure parametric polymorphism so...? What's the point?

[Philip Herron]

This is an ok talk, he needs to hear himself though! He is trying to put across too many complete ideas too quickly i think he is too nervous or something :S. and even at the end i still don't know the point of his talk :S. I mean yeah its nice to think of new ways of abstracting types but its like.. well ok fair enough! I've always found functional languages like haskell are lovely but they are only nice in pure theoretical case. Though i think haskell is the most clever language at the moment!

[SealedSun]

I agree, the first two thirds of the presentation are not very useful. The part on code inference, however, I found very interesting.

[jetong12]

Good upload!