This question already has an answer here:
- ML function of type 'a -> 'b 3 answers
I know for pretty sure that there is a function with the type $f: \forall \alpha, \beta . \alpha \rightarrow \beta$ (at least in a Hindley-Milner type system), but I can't wrap my head over it.
Neither could I think of an actual function with this type.
I found a function of this type, which in Standard ML would be written as:
fun f x = f x
But I am not sure of the lambda calculus equivalent of this function.
Moreover, if I'm right about Curry-Howard, the isomorphism of this type is the proposition $\forall A, B . A \implies B$, which does not make sense for me. Is it possible that someone give a function with type $f$ and explain its Curry-Howard equivalent to me?