1

If I define

fun id x = x

Then naturally id has type 'a -> 'a

Of course, id 0 evaluates to 0, which makes perfect sense.

Since this makes perfect sense, I should be able to encapsulate it by a function:

fun applyToZero (f: 'a -> 'a) = f 0

With the hope that applyToZero will have type ('a -> 'a) -> int and applyToZero id will evaluate to 0

But when I try to define applyToZero as above, SML/NJ gives an odd error message which begins:

unexpected exception (bug?) in SML/NJ: Match [nonexhaustive match failure]
  raised at: ../compiler/Elaborator/types/unify.sml:84.37

This almost looks like a bug in the compiler itself. Weird, but possible.

But PolyML doesn't like it either (though its error message is less odd):

> fun applyToZero (f: 'a -> 'a) = f 0;
poly: : error: Type error in function application.
   Function: f : 'a -> 'a
   Argument: 0 : int
   Reason: Can't unify int to 'a (Cannot unify with explicit type variable)
Found near f 0

The following does work:

fun ignoreF (f: 'a -> 'a) = 1

with the inferred type ('a -> 'a) -> int. This shows that it isn't impossible to create a higher order function of this type.

Why doesn't SML accept my definition of applyToZero? Is there any workaround that will allow me to define it so that its type is ('a -> 'a) -> int?

Motivation: in my attempt to solve the puzzle in this question, I was able to define a function tofun of type int -> 'a -> 'a and another function fromfun with the desired property that fromfun (tofun n) = n for all integers n. However, the inferred type of my working fromfun is ('int -> 'int) -> 'int). All of my attempts to add type annotations so that SML will accept it as ('a -> 'a) -> int have failed. I don't want to show my definition of fromfun since the person that asked that question might still be working on that puzzle, but the definition of applyToZero triggers exactly the same error messages.

Community
  • 1
  • 1
John Coleman
  • 51,337
  • 7
  • 54
  • 119
  • Haskell does support the higher-ranked types that Andreas describes. [Here are some practical use-cases](http://stackoverflow.com/questions/1476480/what-uses-have-you-found-for-higher-rank-types-in-haskell) [StackOverflow]. Minor pedantry: You cannot apply a function to a type in SML, as SML doesn't have type-level functions (or dependent types). – sshine Nov 27 '16 at 23:56

2 Answers2

4

It can't be done in plain Hindley-Milner, like used by SML, because it does not support so-called higher-ranked or first-class polymorphism. The type annotation 'a -> 'a and the type ('a -> 'a) -> int do not mean what you think they do.

That becomes clearer if we make the binder for the type variable explicit.

fun ignoreF (f: 'a -> 'a) = 1

actually means

fun 'a ignoreF (f: 'a -> 'a) = 1

that is, 'a is a parameter to the whole function ignoreF, not to its argument f. Consequently, the type of the function is

ignoreF : ∀ 'a. (('a -> 'a) -> int)

Here, I make the binder for 'a explicit in the type as a universal quantifier. That's how you write such types in type theory, while SML keeps all quantifiers implicit in its syntax. Now the type you thought this had would be written

ignoreF : (∀ 'a. ('a -> 'a)) -> int

Note the difference: in the first version, the caller of ignoreF gets to choose how 'a is instantiated, hence it could be anything, and the function cannot assume its int (which is why applyToZero does not type-check). In the second type, the caller of the argument gets to choose, i.e., ignoreF.

But such a type is not supported by Hindley-Milner. It only supports so-called prenex polymorphism (or rank 0 polymorphism) where all the ∀ are on the outermost level -- which is why it can keep them implicit, since there is no ambiguity under this restriction. The problem with higher-ranked polymorphism is that type inference for it is undecidable.

So your applyToZero cannot have the type you want in SML. The only way to achieve something like it is by using the module system and its functors:

functor ApplyToZero (val f : 'a -> 'a) = struct val it = f 0 end

Btw, the error message you quote from SML/NJ cannot possibly be caused by the code you showed. You must have done something else.

Andreas Rossberg
  • 34,518
  • 3
  • 61
  • 72
  • 2
    Thank you for the detailed answer. I most assuredly got that error message in SML/NJ *version 110.79*. I just looked at the release notes for 110.80 (which I'll download today). Appearing in the list of tracked and fixed bugs is "145 Internal exception occurs on bogus annotation instead of typechecking diagnostic" – John Coleman Nov 26 '16 at 14:11
1

If we use Hindley-Milner type inference algorithm on fun applyToZero f = f 0 we are going to get f : int -> 'a because of the term f 0.

Obviously, f is a function f : 'b -> 'a. We apply this function to 0, thus 'b = int. Hence, the explicit type annotation f : 'a -> 'a produces the error you observe.

By the way, SML/NJ v110.80 works fine on my machine and prints the following error message:

stdIn:2.39-2.42 Error: operator and operand don't agree [overload - user bound tyvar]
  operator domain: 'a
  operand:         [int ty]
  in expression:
    f 0
Anton Trunov
  • 15,074
  • 2
  • 23
  • 43