Talk:Principal type

Woeful description

This is an absolutely horrible description. Full of circularities and gibbberish like "instances of a type". There's a better explanation here:

http://stackoverflow.com/questions/11542446/what-is-a-principal-type — Preceding unsigned comment added by 49.182.133.255 (talk) 06:53, 9 June 2016 (UTC)

There is nothing terribly circular about it. Here's the Pottier & Remy def "a principal type scheme is least specific in the sense that all valid types are substitution instances of it." from *The Essence of ML Type Inference*. What this page needs are perhaps some examples.

And yeah, the French are trying to be super correct mathematically by intro'd kinds and type schemes, and identifying schemes without type variables with the underlying types. Hindley himself doesn't bother with that in *Basic Simple Type Theory*. He just defines what it means for a type to be an instance of another via type substitution, in which one can replace type variables with types. However, such a def is unsatisfactory outside ML. For instance, intersection types have no type variable themselves, but there is a notion of 'substitution', or rather of subtyping involved, which yields a principal type as well. So, yeah, perhaps the article could explain that what is meant by 'instance' is in fact a little tricky, and depends on the type system involved. Wells manages to give a general definition for typings in terms of program fragments, but I'd loathe to WP:OR the equivalent for principal type because he alas doesn't define principal type.