For a bit of theoretical background, try http://www.cl.cam.ac.uk/teaching/1415/Types/types.notes.pdf http://www.cl.cam.ac.uk/teaching/1415/Types/types.notes.pdf

For a bit of theoretical background, try http://www.cl.cam.ac.uk/teaching/1415/Types/types.notes.pdf http://www.cl.cam.ac.uk/teaching/1415/Types/types.notes.pdf (it's fairly easy reading). I'm not sure I quite understand what you're saying completely, but typically we distinguish types from values because we otherwise find it very difficult to write a performant typing algorithm. Personally, I try to avoid subtyping where possible; I usually end up getting weird contradictions.