型の意味

JcentricTSのような簡単な型システムでも、型の意味はけっこう複雑で、Uをアンビエント対象＝JSON領域だとして：

1. 台型の表現空間R、これはposetoid
2. 台型の表現空間上で定義された3値述語p、⊥付きbooleanへのposetoid射
3. 台型の値空間V Q(R)と同型だが同じとは限らない
4. 値写像v:R→V
5. 台型の表現空間RのUへの埋め込みe:R→U

むずかしいはずだわ。