-
carbon_twelve
- 1177
- 0
- 0
- 0
-
- いいね！0
FLタイプシステム続き
型体系の拡張
ネクタイ
@carbon_twelve
2.深さ方向。{x:int, y:int, color:{r:int, g:int, b:int}} <: {x:int, y:int, color:{r:int}}。 #言語モデル論
2012-01-16 10:27:35※記法を統一するためにツイートを差し替えました。「Γ⊦M:τ」は「型環境Γの下で式Mの型がτである」という意味であり、「(rule) A | B」は「Aから規則ruleを用いてBを推論することができる」という意味です。
(S-list) σ<:τ | list(σ)<:list(τ)
(S-rec) σ_1<:τ_1,...,σ_n<:τ_n | {l_1:σ_1,...,l_(n+m):σ_(n+m)}<:{l_1:τ_1,...,l_n:τ_n}
(S-top) | τ<:Top
(S-abs) τ'<:σ', σ<:τ | σ'→σ<:τ'→τ
XENO
@xenophobia__
ラムダ抽象の型階層規則「σ<:τ、τ’<:σ’⇒σ’→σ<:τ’→τ」は結果型に関しては共変(covariant)、引数型に関しては反変(contraavariant)になっている。 #言語モデル論
2012-01-16 10:33:40