Home » forums » LtU Forum

Google Tech Talk: Phil Gosset discusses parametric polymorphism and girard-reynolds isomorphism

http://video.google.com/videoplay?docid=-4851250372422374791&q=user%3A%22Google+engEDU%22&hl=en

Enjoy.

By Chris Perkins at 2007-04-25 04:28 | LtU Forum | previous forum topic | next forum topic | other blogs | 7870 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Wadler's blog

This was the subject of a post in Phil Wadler's blog, where he points corrections to some technical errors in the presentation.

By Andrei Formiga at Wed, 2007-04-25 16:41 | login or register to post comments

Link

Phil's blog post is here.

By Anton van Straaten at Wed, 2007-04-25 17:00 | login or register to post comments

Regarding Phil's Comment at the End

I showed the lecture to a friend and he asked a valid question which I didn't have an adequate answer for, and it intrigued me as well.

During the last few minutes of the lecture, Phil comments that he uses Girard-Reynold's Isomorphism while programming by writing in a comment the type of the expression. Then after programming, he looks up the type and compare it to the comment.

My friend's question is: Why comment out the type? You might as well declare the type and let the compiler compare it for you.

Is there any insight we might have missed?

Ohad.

By Ohad Kammar at Fri, 2007-04-27 15:50 | login or register to post comments

I imagine it's reuse

By giving a comment, you document what the expectations of the type inference should be. Uncommenting the type annotation may end up restricting the genericity of the function. Or it may end up restricting the types of other functions in the unification process.

Basically he's saying that he wants genericity but with some comments about what the limits are when the code was constructed.

By Chris Rathman at Fri, 2007-04-27 16:39 | login or register to post comments

maybe an experiment

I only watched the first five minutes of Phil's talk (during which I learned how one pronounces "Principia"; I'm one of those readers who knows many, many words I've never heard anyone say aloud).

But your description of Phil's technique sounded like an experiment to me, intending to verify one's own independent reasoning, to get two readings on a value that should be the same, so each can verify the other. (So I thought your friend's question was similar to asking why double blind studies are better than open studies where expected results are known.)

There's a very good reason to do this, which isn't obvious from the academic result of getting a match after minimizing bias during an experiment. But even this part is valuable as a test cycle: a type match is the same as passing a runtime test in terms of giving you a data point on quality.

I've found that quality of code is often directly related to how much thought has gone into reasoning about whether it will work as intended, and the most effective reasoning is one that happens in your mind, and not in a tool. (A person considers many more ancilliary lines of reasoning than a minimal set necessary, and these end up informing other understandings about code, often giving insight into good and bad options like simplifications and risks.)

By Rys McCusker at Fri, 2007-04-27 17:17 | login or register to post comments

Regarding Phil's Comment at the End

The other comments are essentially what I had in mind.

This relates to a concept I meant to mention in the talk. The "principal type" is the most general type of a given term. You might have over-specified the type signature, and won't otherwise see that. By commenting out the type first, the type inference algorithm in GHCI will give you the actual principal type, which might not be what you expected.

By Phil Gossett at Sat, 2007-04-28 19:41 | login or register to post comments