Type system primer

Given an expression e, a type T and a dictionary TT
that maps variables to type, the notation

TT |- e : T

roughly means

T = typecheck(TT, e)

and the horizontal bar notation:

P1     P2     P3
----------------
      Q

means

Q if P1 and P2 and P3

from: http://wiki.jvmlangsummit.com/pdf/28_Siek_gradual.pdf (slide 6)