For those who don't realise, the challenge is to write a function `f` that takes three arguments, the first of which is a function which is applied to the second and third arguments and returned in a pair.

The difficulty with doing this in a statically typed system is that once you've fixed the type of the function you pass in, you can't then apply it to two different types. The standard way to solve this would be to specify that the function you pass in is valid for all types [1]

    f :: (forall s. s -> s) -> a -> b -> (a,b) -- [2]
    f r a b = (r a, r b)

    f id 5 "Test"   -- returns (5,"Test")

However, the challenge also specified that you do it without writing a type signature for `f`. I admit that in this case I am pretty stumped. The closest I can get is to first define a wrapper

    data S = forall a. Show a => S a
    instance Show S where Show (S a) = show a

and then write

    f r a b = (r a, r b)

    f id (S 5) (S "Test")    -- returns (5,"Test")

but that involves wrapping everything up before passing it into the function, to disguise the fact that we really have different types.

There's an interesting point to be made here, though - "wrapping everything up in one type" is essentially what dynamic type systems do, except that it's baked into the language instead of being implemented by the programmer on an as-needed basis.

Here, my declaration for the type S says "any type as long as it has a Show instance" (which allows it to be printed). I could instead have specified "any type that has a Num instance" which would mean that I could pass in a mix of ints and floats, and still do arithmetic with them. I get some of the benefits of dynamic typing (flexibility) but I still get to keep type checking.

The Python approach is "any type, and we'll check at runtime that it has the appropriate methods". So it's ultimately flexible, but as a result loses any form of compile-time checking.

Looking at it this way, I think that the challenge you've set me is one that cuts to the core of the difference between dynamic and static type systems. No, I can't write the function you want in a statically typed language without doing something clever with types. But the clever thing I have to do with types is re-invent duck typing, but in a limited way which still gives me compile-time checking.

Anyhow, thanks for the insightful comment. It certainly made me think...

[1] This requires the language extensions ExistentialQuantification and Rank2Types, but neither of those are particularly controversial.

[2] Note that the type signature

    forall a. a -> a

is inhabited by exactly one function - the identity function. This carries over to the Python example too - the function `f` isn't safe to use unless the first argument is the identity function, which makes it a bit of a useless function to define in the first place.

That's actually the only place ML^F ever requires type annotations - when you want to take a polymorphic function as argument and use it at different types. MLF is basically as strong as inference for polymorphic types gets, so it's not surprising annotations might be needed here too. (intersection types handle the example nicely, but I don't know of any languages using them).

If you want to faithfully translate the idea that 5 and "Test" are different values that can be passed into the same places but told apart by tests if you want, you might translate the second line to something like f (\x -> x) (Left 5) (Right "Test"), which does pass.

One useful distinction I make is between types and datatypes. Types are a mathematical theory in which you are able to prove things about the terms of you program.

Datatypes are like types but without the structure or logic. They don't prove anything and are basically just sets. You have to bring your own rules. Dynamic languages are unityped, you can see this by noting working only on just a top type shares many properties (not all, e.g. flexibility) of being in a dynamic language. Dynamic languages however can have datatypes, which make sure operations on the collections a particular object inhabits makes sense according to rules the language designer defines.

For your example, in a dynamic language I can state that r,a and b all belong to the same type but their datatypes may vary from moment to moment. In a statically typed language I cannot. Without types a ST language will assume that a and b are the same universal type. But I could give just a a top type and then your example would work. But I lose type safety. To get it back I could use interfaces, inheritance or algebraic datatypes each with their own pros and cons.