First, some remarks. Using only the core typed lambda calculus it's not possible to obtain 'a -> 'b
because the typing system is in correspondence (via the Curry Howard isomorphism) to intuitionistic logics, and the corresponding formula A → B
is not a tautology.
Other extensions such as tuples and matchings/conditionals still preserve some logic consistency adding product types *
which correspond to the logical connective and, and sum types |
which correspond to the or. Again, don't expect them to produce that 'a -> 'b
type, as it would allow one to prove some formula which is not a tautology.
So your only chances are using other constructions which escape from the logics like raise
(but you're not allowed to in this case)… or let rec
! Recursion allows to build programs which never terminate, and their results can be given an arbitrary return type as they will never be produced. Now if you think about the most trivial non terminating function (the one which directly calls itself to return a result):
let rec f x = f x
You'll notice that its type is exactly 'a -> 'b
: whatever is the provided argument, the result (which will never be computed) can be assumed to have any type.
Of course this f
is not an interesting function, but that's the point. In OCaml, any function whose type does not look like a valid formula is a suspicious function.
raise
would work, so we know how best to explain why the solution your prof is looking for (which will work for the same reasons thatraise
works) works. $\endgroup$ – sepp2k Mar 13 '12 at 11:29raise : exn -> 'a
so I can get the return value, I just ignore the argument. $\endgroup$ – Gilles 'SO- stop being evil' Mar 13 '12 at 12:00