Hi Tillmann, On Wed, Apr 3, 2013 at 11:59 PM, Tillmann Rendel wrote:

From the type-theoretic point of view, I guess this is related to your view of what a polymorphic function is.

Do you have a reference to the previous conversation?

but we moved further and further towards the System-F-ish view that polymorphism is an explicit, computational thing.

While that may be true, I read the original email as merely referring to the explicit annotation of types (where they are customarily neither seen nor written) as a particular pedagogical approach for new students, something which has much to recommend for. Which seems miles away from what you're alluding to. Full-blown type-level programming? Operational semantics at the type-level? I'm not sure. -- Kim-Ee

On 4/04/2013, at 5:59 AM, Tillmann Rendel wrote:

As I understand it, in ML, it seemed to be a clever idea to not have type signatures at all.

Wrong. In ML, it seemed to be a clever idea not to *NEED* type signatures, and for local definitions they are very commonly omitted. But you can certainly HAVE type signatures, and for modules ('structures') it is normal to have them in the interfaces ('signatures'). signature SOME_SIG = sig val f : int -> int list -> int val a : int end structure Some_Struct : SOME_SIG = struct fun f i [] = i | f i (x:xs) = f (i+x) xs val a = 42 end What ML does not have is type *quantifiers*. For that matter, you could say that ML has one type class: Eq.

On 5/04/2013, at 1:22 AM, Tillmann Rendel wrote:

Hi,

Richard A. O'Keefe wrote:

...

...

As I understand it, in ML, it seemed to be a clever idea to not have type signatures at all.

Wrong. In ML, it seemed to be a clever idea not to *NEED* type signatures, and for local definitions they are very commonly omitted.

In the ML I used, I remember that it was syntactically impossible to use type signatures directly adjacent to a local definition.

Notice that the goal-posts just got moved far far away. The original complaint was that ML did not allow type signatures. Now the complaint is that it does not allow them to be "directly adjacent".

Instead, I was thaught to put something like a type signature in a comment, approximately like this:

(* getOpt : 'a option * 'a -> 'a *) fun getOpt (SOME x, y) = x | getOpt (NONE, y) = y

Well, that's a bit silly, isn't it? Put getOpt in a structure where it belongs, and the type in the signature, where the compiler can enforce it. A type signature that is not enforced is a type signature you cannot trust.

...

But you can certainly HAVE type signatures, and for modules ('structures') it is normal to have them in the interfaces ('signatures').

In my opinion, a signature for a structure would not count as "directly adjacent". Also, while I don't know much about the history of ML, I suspect that structures and signatures were a later addition to the core language.

The history of ML is not so hard to find out. Structures and signatures have been part of "Standard" ML since the 1980s. The ML in Edinburgh LCF and Luca Cardelli's VAX ML were significantly different languages from SML, but VAX ML at least did have modules. The distinction between "Core" and "Modules" in old SML documentation has to do with convenience of specification more than anything else.

I just checked Milner, Tofte and Harper, The Definition of Standard ML, MIT Press 1990 (available at http://www.itu.dk/people/tofte/publ/1990sml/1990sml.html),

That's the old out-of-date edition. The current version of the language is SML'97. However, this much is the same: - there are declarations that provide *interfaces* (grammatical category "spec" -- see page 13), which may occur in signatures - and declarations that provide *values* (grammatical category "dec" -- see page 8), which may occur in structures, at top level, and elsewhere So it is definitely true that, by design, SML "type signatures" (strictly speaking, "valdescs") are segregated from SML function definitions ("valbinds" or "fvalbinds"). This is pretty much a consequence of SML having a very expressive module system in which modules _have_ signatures.

and learned that we can have explicit type annotations for both patterns and expressions, so the following variants of the above are possible in Standard ML:

1. We can embed parts of the signature into the definition:

fun getOpt (SOME (x : 'a), y : 'a) : 'a = x | getOpt (NONE, y : 'a) : 'a = y

Perhaps better: fun get_opt (SOME x, _) = x | get_opt (NONE, y) = y val getOpt : 'a option * 'a -> 'a = get_opt which can be written local fun getOpt(SOME x, _) = x | getOpt(NONE, y) = y in val getOpt: 'a option * 'a -> 'a = getOpt end

With decomposing the type signature into its parts, and then duplicating these parts, this is not very attractive.

This is a sure sign that you are NOT using the language the way it was intended to be used, and maybe it isn't the language that's wrong.

2. We can do better by avoiding the derived form for function bindings:

val getOpt : 'a option * 'a -> 'a = fn (SOME x, y) => x | (NONE, y) => y

This looks ok to me, and I wonder why I was not thaught this style,

Because it is atrociously ugly. (Aside.) "val" here should be "val rec" in general. (End Aside). ML is designed to have type specifications for functions *inside signatures*. Since functions are supposed to be declared inside structures, and structures are supposed to *have* signatures, it would be rather silly to write function type specifications twice. So ML is *not* designed to encourage you to do that.

On 13-04-03 07:39 PM, Alexander Solla wrote:

There's your problem. Mathematicians do this specifically because it is helpful. If anything, explicit quantifiers and their interpretations are more complicated. People seem to naturally get how scoping works in mathematics until they have to figure out free and bound variables.

Quantifiers are complicated, but I don't see how explicit is more so than implicit. If anything, it should be the other way round, since correctly interpreting the implicit case incurs the extra step of first correctly guessing how to explicate. (If it doesn't have to be correct, I know how to do it 100 times simpler, to paraphrase Gerald Weinberg.) I have just seen recently prove or disprove: for all e>0, there exists d>0, if 0

On Thu, Apr 04, 2013 at 11:02:34AM +0000, Johannes Waldmann wrote:

My feeling is that mathematicians use this principle of leaving out some of the quantifiers and putting some others in the wrong place as a cultural entry barrier to protect their field from newbies.

Albert showed an example of leaving out quantifiers, but I didn't see an example of quantifiers in the wrong place. Did I miss one? Tom

On Thu, Apr 04, 2013 at 01:15:27PM +0000, Johannes Waldmann wrote:

Tom Ellis writes:

...

I didn't see an example of quantifiers in the wrong place.

The example was:

...

every x satisfies P(x,y) for some y

Oh I see. I interpreted that as lack of disambiguating parentheses, but it's not unreasonable to assert that quantifiers should always come before formulas. Syntax certainly is hard. I remember being completely puzzled the first time I saw / | dx (long expression in x) / when I expected / | (long expression in x) dx / (Those are integral signs, by the way!) Tom