1

Usually test which contain question about SML have questions that ask you to find the signature/type of a function.

For example - What is the type of the following function:

fun foo f g x y = f (f x (g x) y) y;

Solution:

val foo = fn : ('a -> 'b -> 'b -> 'a) -> ('a -> 'b) -> 'a -> 'b -> 'b -> 'a

I was wondering if there is a good algorithm I could follow in order to solve those kind of questions. Every time I try to solve one of those, I get confused and fail.

vesii
  • 2,760
  • 4
  • 25
  • 71
  • SML uses the [Hindley-Milner Algorithm](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system) for type inference, but somehow I don't think that you are asking for an actual algorithm so much as an easy heuristic. If so, that is too vague of a question. – John Coleman Jan 26 '19 at 03:29
  • Possible duplicate of [Hint for SML type inference](https://stackoverflow.com/questions/37640686/hint-for-sml-type-inference) – sshine Jan 28 '19 at 06:37
  • 1
    @SimonShine I don't think it is a duplicate (although they are similar) since the other question was for some specific examples and this question is more about the general approach. It is perhaps a bit too general, but since molbdnilo has given a helpful answer I think I will retract my "too broad" close vote. – John Coleman Jan 29 '19 at 17:20
  • I've seen this question a few times, being "How do I perform type inference?" and "... given this practical example." The last time I answered [a question like this](https://stackoverflow.com/questions/46044213/sml-type-inference-by-hand), I linked to five other examples of the question. So if the question was general, it'd warrant an answer, and if it's help with a concrete example, it seems that they're generally not used. Perhaps, instead of voting to close with "duplicate of", I should simply link to the existing questions, since one of the other concrete examples may be similar enough. – sshine Jan 30 '19 at 12:39
  • Also, I appreciated and upvoted @molbdnilo's answer. I don't generally mind that SML questions are homeworky, since that appears to be the destiny of SML. :-) – sshine Jan 30 '19 at 12:41

2 Answers2

2

Start with what you know, then figure out a bit here and a bit there until there are no unknowns.

Here is one possibility:

Call the unknown types FOO, F, G, X, and Y, respectively.

Then look for something small and easy and start assigning types.

(g x)

is clearly an application of a function to one argument.
Set X = a and G = a -> b.

Then look at the enclosing expression:

(f x (g x) y)
   |   |
   v   v
   a   b

So far, we know that F = a -> b -> Y -> C, for some C.

Go outwards again:

f (f x (g x) y) y

Since both x and (f x (g x) y) are first arguments to f, they must be the same type a, and the same idea applies to y and (g x), giving them the type b.

So, F = a -> b -> b -> a and, since the outer f is only given two arguments, the type of the right-hand side must be b -> a.

Thus

X = a
Y = b
G = a -> b
F = a -> b -> b -> a
FOO = (a -> b -> b -> a) -> (a -> b) -> a -> b -> (b -> a)

And, since arrows associate to the right, FOO is equivalent to

(a -> b -> b -> a) -> (a -> b) -> a -> b -> b -> a
molbdnilo
  • 64,751
  • 3
  • 43
  • 82
0

There are several ways to derive the type of a function depending on how close to the compiler's algorithm you want to go and how much you want to cut corners with intuition, which can come handy in practice and perhaps in exams, depending on the focus of the exam.

  • An example by Ionuț G. Stan cuts very few corners, and has a quite verbose notation. This mechanical approach is very safe, spells out everything and takes some time.

  • This current example by molbdnilo takes a middle ground and does some equational reasoning, but also relies on some level of intuition. I think this is generally the way you want to be able to do it, since it takes less time and space by hand.

  • An example by me links to various other examples for a diversity in practical approaches.

sshine
  • 15,635
  • 1
  • 41
  • 66