"On understanding types, data abstraction, and polymorphism" (1985) by LucaCardelli and PeterWegner

http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.117.695

This paper gives definitions for several different forms of PolyMorphism, like ParametricPolymorphism and AdHocPolymorphism. (These terms were originally coined by ChristopherStrachey.)

Available from LucaCardelli's home page and other places.

''Does anybody have a comment about whether the given definitions or models in this work lean toward a dynamic or static view of language typing? My observation is that formal definitions of types and objects lean toward a static view, perhaps because it is easier to "do math" on something static.''

That's not why. The reason is to provide static type safety: to provide guarantees of type correctness. If an analysis of type correctness cannot be completed statically, then one must run the program partially or wholly without knowing whether it is type correct, which means that in fact it might demonstrate type '''incorrectness''' at any time during its run.

Dynamic type checking can prevent meaningless operations from being executed, but in the general case, only at the expense of aborting execution (the fact that execution does not need to be aborted in special cases is irrelevant).

This can be a Very BadThing, as with e.g. the Ariadne rocket failure. -- DougMerritt

----
''In the case of "critical" applications such as rockets, missiles, and medical equipment; I agree that static strong typing is a net benefit. However, this may not be the case in other domains, which may benefit from dynamic and/or "light" typing. I believe that the features-per-coding-hour is higher with dynamic languages, but so is the bug count, in general (excluding unit tests for now). If the feature count is more important to the domain requirement profile[1] than the bug count, then the dynamic approach may be considered the more economical choice. (There are other topics on this, and I'll add links as I re-encounter them.) --top''

It sounds like you have an understanding of what types are, because you admit that there are languages with strong/static typing, and other ones with light typing. As for features-per-coding hour, there are languages which claim to be as easy to use as dynamic languages, but still have static/stronger typing systems. One of these is GoProgrammingLanguage.  In the video, Rob Pike says something about GoProgrammingLanguage being as easy to use as a dynamic language, but with strong/static typing.  Personally, I don't understand why dynamic languages are considered easier - I consider them different, not easier. Delphi, a strong typed language, is very easy and clear code. I found PHP code much harder to read and program in. Maybe this is personal taste.

In order to understand types, I think one has to start out with an educational language that actually makes clear distinctions between types, variables, and values. I think StandardPascal does a good job of distinguishing types, variables, and values. Just because StandardPascal is not in use, doesn't mean it cannot be used to educate a person on what a variable, type, and value are.  The C language doesn't make clear distinctions, because variable declarations are mixed with code. The BasicLanguage is not good for distinguishing types, variables, and values either.

''There are other topics on the pros/cons of dynamic versus static or strong versus weak typing etc. I don't wish to reinvent those arguments here in the spirit of OnceAndOnlyOnce and will thus refer the reader to CategoryTypingDebate.''

This page is about understanding what types are. In order to understand what types are, a programming language that makes a clear distinction between types, variables, and values is needed. How else is one going to understand types? Referring to verbose TypeTheory books?

''There's no clear-cut definition. People can study a million examples together and probably come fairly close to agreement, but there's still no clear-cut definition after all that.''
-------
[1] It is argued by some that managers and organization decision makers often don't understand the real cost of bugs, and thus under-count their value. I am generally skeptical of this argument, but it's an open and difficult question that deserves further research. Understanding the actual needs of the "customer" is often a bigger bottleneck than the presence of bugs. Doing the wrong thing right is often at least as bad as doing the right thing wrong. In my observation, dynamic languages better facilitate the trial-and-error process that is sometimes needed to figure out what the customer really wants. It's too expensive to do such trial-and-error with heavy-typed languages. They require more BigDesignUpFront to pay off.  -t
----
CategoryPaper, WhatAreTypes, CategoryPolymorphism, DefinitionsOfTypes CategoryTypeTheory