型システム

型なし､単相型､一階多相､n階多相､線形型､型関数､依存型など､強力な型があればあるほど静的に安全性を保証できる範囲が広がる一方､型の不一致が起きてないかどうかの計算が複雑になり､型が正しいかどうかの証明を与える必要があるなどのトレードオフがある｡