主要型（principal type）のある体系とは、以下の性質を満たすような体系です。 型環境と項が与えられた時、につく型（一般に複数ありうる）は、何らかの型を具体化したものになっている。 一方、主要型付け（principal typing）のある体系とは、以下の性質…