3
$\begingroup$

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?

Improve this question
$\endgroup$
0

2 Answers 2

Reset to default
5
$\begingroup$

Think of this in terms of the Curry-Howard isomorphism. What would this type look like as a theorem?

  • For any propositions $A$ and $B$, $A \implies B$.

Clearly this is not true, if it were, then we could do $A=\top$ and $B = \bot$ and now true implies false! So, if it's not a true theorem, there's no proof of it, so the type is uninhabited.

In a language like Haskell or SML, you write a function of this type, as long as it doesn't terminate or is undefined:

myfun x = undefined
> myfun :: t -> t1

but in a total language with a sound type system, this should not be possible.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ Indeed. I found my definition of f in SML was essentially uninstantizable. $\endgroup$
    – xuq01
    Commented Feb 6, 2017 at 22:55
5
$\begingroup$

I know for pretty sure that there is a function with the type $f: \forall \alpha, \beta . \alpha \rightarrow \beta$, but I can't wrap my head over it.

No, that type is not inhabited. There are no functions having that type in a typed lambda calculus, provided it is (weakly) normalizing.

The intuition is that, as you mention, the associated proposition is clearly not a theorem.

More in detail, if we had an inhabitant $f : \forall \alpha, \beta . \alpha \rightarrow \beta$, then we would have $$ \lambda \alpha. f (\alpha\to\alpha)\alpha(\lambda a:\alpha. a) \ :\ \forall\alpha.\alpha $$ hence every type would be inhabited, making our system inconsistent -- but we know that's not the case.

By the way, what makes you think there should be such an $f$? Even in everyday programming, we can't really convert a value of a type $\alpha$ to any other arbitrary type $\beta$.

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.