Lambda the Ultimate

inactiveTopic Putting Type Annotations to Work
started 8/7/2002; 8:19:20 AM - last post 8/7/2002; 7:30:15 PM
Ehud Lamm - Putting Type Annotations to Work  blueArrow
8/7/2002; 8:19:20 AM (reads: 1752, responses: 3)
Putting Type Annotations to Work
Putting Type Annotations to Work. Martin Odersky, Konstantin Läufer, Conference Record of POPL '96

We study an extension of the Hindley-Milner system with explicit type scheme annotations and type declarations. The system can express polymorphic function arguments, user-defined data types with abstract components, and structure types with polymorphic fields...

Heavy stuff, but important if you are interested in thing like Rank-2 polymorphism etc.

And you should be interested, since all programming is about choosing the appropriate level of polymorphism, and finding the progrsmming technique that let's you achieve it.


Posted to theory by Ehud Lamm on 8/7/02; 8:19:57 AM

Jay Han - Re: Putting Type Annotations to Work  blueArrow
8/7/2002; 9:12:42 AM (reads: 723, responses: 1)
And you should be interested, since all programming is about choosing the appropriate level of polymorphism, and finding the progrsmming technique that let's you achieve it.

Please elaborate?

Paul Snively - Re: Putting Type Annotations to Work  blueArrow
8/7/2002; 7:30:15 PM (reads: 696, responses: 0)
I'll bite.

You want print() to do the right thing (whatever you think that is) regardless of whether its parameter is a string, an integer, a floating-point number... that's polymorphism. It lets "print" be a good name (descriptive of the operation being performed) vs. a collection of less-good names (printString, printInt, printFloat...) that talk about their arguments instead of what they're doing with their arguments.

One of the major principles of programming is the Principle of Least Surprises: given a new type, print() should work, and work as expected, on a value of that type. Much of programming language design revolves around the various approaches to getting as near to that goal as possible.

Ehud Lamm - Re: Putting Type Annotations to Work  blueArrow
8/8/2002; 2:20:14 AM (reads: 728, responses: 0)
A large part of programming is concerended with the tension between flexibility and generality on the one hand, and simplicity and efficiency on the other hand. Essentially, it is about deciding just how general/generic or polymorphic your code shold be.

Another way of looking at this is saying the software design is about choosing the right level of abstraction. Thre abstraction level determines, to a large extent, the polymorphicity of the code.

Note: I use the terms generic and polymorphism quite loosely here. Don't hold it against me.