Is expression evaluated before assigning type?

Question

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?

Answer 1

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.