Reify PTS & implement language subtyping, v2

Updated version of #113.