I am assigning type to an $\lambda$-expression: if false then M else N where if A then B else C and false have their usual meanings (read: not specified).

The problem arises because M and N have different types. While clearly the expression evaluates to N & hence should be assigned type(N) but apparently it is expected that for if-else, the types for B & C should be same.

How to proceed on this? Should I use conjuncted type?

  • $\begingroup$ What do you mean by conjuncted type? $\endgroup$ – Potato44 Mar 30 at 12:00
  • $\begingroup$ I may have used the word "conjunction" incorrectly. I'm referring to this answer $\endgroup$ – Sudutt Harne Mar 31 at 17:41
  • $\begingroup$ That sounds like intersection types. Do you also have union types? $\endgroup$ – Potato44 Mar 31 at 17:42
  • $\begingroup$ No, I don't think we have covered them yet. $\endgroup$ – Sudutt Harne Mar 31 at 17:46

Type checking is something that happens before evaluation.

In most common type systems for lambda calculus, including simply typed lambda calculus and System F, if false then M else N is ill typed if N and M have different types. Unless you have been told otherwise you are probably working with one of these.

There are extensions such as union types and certain forms of subtyping that allow if false then M else N to be well formed with N and Mhaving different types.

  • $\begingroup$ Thanks for the explanation! Could you suggest some books/authoritative references to study this further from? $\endgroup$ – Sudutt Harne Mar 31 at 18:34
  • $\begingroup$ I haven't read either myself, but two I have seen recommended by others are " Practical Foundations for Programming Languages" by Robert Harper and " Types and Programming Languages" by Benjamin Pierce. $\endgroup$ – Potato44 Mar 31 at 20:43

Your Answer

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

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