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...
Oh, I'm in This part of youtube Again....
Was just looking for repeat episodes of the big bang theory....
Bounce0Up0Nessa3 1 month ago
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.
RandomRemarks 5 months ago
@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 1 year ago
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?
tohopes 1 year ago
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!
redzor812 1 year ago
I agree, the first two thirds of the presentation are not very useful. The part on code inference, however, I found very interesting.
SealedSun 2 years ago
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.
twifkak 3 years ago
Good upload!
jetong12 3 years ago
0 comments?
gekorio 3 years ago