それよりもよー、
型付きλ計算の型と、
「プログラミング言語における型」の違いがよく分からんのだが。