We are given a simple functional language:

$ e ::= x | n | e_{1}e_{2}|\lambda(x:\tau).e$

with types:

$\tau ::= \text{int} | \tau_{1} \rightarrow \tau_{2}| \tau_{1} \land \tau_{2} $

Is the expression $ (\lambda x.xx) (\lambda y . y) $ typeable in this system?

Let's denote $x:\tau_{x}, xx : \tau_{xx}$. I'm rookie in the field and so far I have only dealt with very simple systems where type equations as the one we get for left subterm: $\tau_{x} = \tau_{x} \rightarrow \tau_{xx}$ indicated a term analyzed is not typeable . The type $\tau_{1} \land \tau_{2}$ is something new to me and I don't have intuition what can or cannot be done here.

  • 2
    $\begingroup$ Search "intersection types" on this site, I think you'll find useful information. The answer is yes because all strongly normalizing terms are typable. $\endgroup$ – Gilles 'SO- stop being evil' Jun 15 '19 at 15:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.