前章では範囲限定抽象型9t<: : を独立した型構成方法として扱った．実際，実用 的な観点からは，抽象型は情報隠蔽という他の型構成方法で作られる型とは全く異な る用途を持っているので，それを独立した型構成方法として取り扱うのは極めて妥当 である．しかし，理論的な分析に於いては，例えば或る言明を型の構文に関する構造 的帰納法での場合分けによって証明する状況を考えれば判る通り，独立した型構成方 法が少なければ少ない程，分析は簡潔に行なえる．そこで，本節では，範囲限定抽象 型9t<: : の範囲限定多相型8t<: : と関数型 ! とによるコード化に関して検討 する．
このコード化そのものは古くから良く知られた事実である．実際，2階の命題論 理に於いての2階の存在限量子9の2階の全称限量子8と含意とによるコード化 については，例えば，自然演繹法に関する代表的文献であるPrawitz (1965)で具体 的にコード化方法が与えられている．また，プログラミング言語論の世界でも例えば
Reynolds (1983)は抽象型が多相型と関数型とでコード化可能な事を示した．
しかしながら，抽象型に対応する式構文（pack式とunpack式）の側のコード化 が多相型と関数型とに対応する式構文によって具体的にどの様に行なわれ，それが型 の側のコード化に基づく推論規則の組み立てに対して健全となるか，という事は，調 べ得た限りでは具体的に証明された事は皆無である．更に，Funの様な束縛型変数 の取り得る型の範囲限定を許す場合，抽象型構成子を多相型構成子と関数型構成子と で具体的にコード化できる事を示した論文も存在していない．
それ以上に重要な事は，限量化での範囲限定を許す場合，範囲限定のない場合に知 られている上記のコード化を実際に適用すると，コード化の為に導入される新しい型 変数を扱う為に，従来は知られていない推論規則が不可欠である事が判明する．
そこで，本節では，範囲限定を許した抽象型9と関連する式構文を多相型8と関 数型!（やそれらに対応する式構文）とによって具体的にコード化を行ない，その コード化が前章で示した部分型関係や型付けに関する推論規則に関して整合的である 事を示し，更に，その証明の中で，従来は知られていなかった新たな推論規則が必要 となる事を示す．
抽象型9t<:: と関連する式構文であるpack式およびunpack式を以下の 様に定義する：
9t<:: ,8s<:Top:((8t<::( !s))!s);
pack
9t<::
ewith,3s<:Top:x:8t<::( !s):x[]e;
unpacke
1
asxwithtine
2 ,e
1
[](3t<::x::e
2 ):
ここで，最後の式の中の型は式e2 の型であり，型 は式e1 の型9t<::
中のそれである．
抽象型の多相型と関数型とによるコード化を定義 3.1に示す．以下，前章で与えた 抽象型に関する様々な推論規則がこのコード化に対して矛盾していない事を示す．
定理 3.2（抽象型のコード化の整合性）
前章での抽象型に関する推論規則 [S-EXIST], [T-PACK], [T-UNPACK],
[A-9
], [A-PACK], [A-UNPACK]の何れもは，上のコード化の下で他の公理 や推論規則によって導出可能である．
証明
各々の推論規則に対する導出を具体的に与える事によって証明する．なお，導出木 中の\y"と\z"とは，各々，[S-WEAK]則と[T-TWEAK]則との適用である（これ らの推論規則の適用に関しては，本証明の後の議論を参照されたい）．
[S-EXIST]則の導出：
C[t<:].<:
0
(y)
C[s<:Top][t<:].<:
0
C[s<:Top][t<:].s<:s
C[s<:Top][t<:]. 0
!s<:!s
C[s<:Top].8t<::(
0
!s)<:8t<::(!s) C[s<:Top].s<:s
C[s<:Top].((8t<::(!s))!s)<:((8t<::(
0
!s))!s)
C.8s<:Top:((8t<::(!s))!s)<:8s<:Top:((8t<::(
0
!s))!s)
[T-PACK]則の導出：
C[s<:Top];0[x:8t<::(!s)]; 1.x:8t<::(!s)
C.<:
(y)
C[s<:Top].<:
C[s<:Top];0[x:8t<::(!s)];1.x[]:[t:=]!s
C;0; 1.e:[t:=]
(z)
C[s<:Top];0; 1.e:[t:=]
C[s<:Top];0[x:8t<::(!s)]; 1.e:[t:=]
C[s<:Top];0[x:8t<::(!s)]; 1.x[]e:s
C[s<:Top];0; 1.( x: 8t<::(!s):x[]e):(8t<::(!s))!s
C ; 0; 1.(3 s<:Top:x: 8t<::(!s):x[]e):8s<:Top:((8t<::(!s))!s)
[T-UNPACK]則の導出：
C ;0;1.e
1
:8s<:Top:((8t<::(!s))!s) C.<:Top
C ;0;1.e
1
[]:(8t<::(!))!
C[t<:];0[x:];1.e
2 :
C[t<:];0;1.(x::e
2 ):!
C ;0;1.(3t<::x::e
2
):8t<::(!)
C ;0;1.e
1
[](3t<::x::e
2 ):
[A-PACK]則の導出：
[T-PACK]則の導出と同様．
[A-UNPACK]則の導出：
[T-UNPACK]則の導出と同様．
[A-9
]則の導出：
紙幅の関係で，帰結部の不等式の導出に関してのみ以下に示す：
(3s<:Top:(x:8t<::(
1
!s):x[]e
1 ))[
2
](3t<::x:
1 :e
2
) 定義3.1でのコード化による
6(x:8t<::(
1
!
2 ):x[]e
1
)(3t<::x:
1 :e
2
)
[A-8 ]による
6(3t<::x:
1 :e
2 )[]e
1
[A-! ]による
6(x:
1
[t:=]:e
2
[t:=])e
1
[A-8 ]による
6e
2
[t:=][x:=e
1
]
[A-!
]による．
完全な形の導出木は，以上の不等式の導出の各ステップでの推論規則の適用に適当 な型付け文脈を補い，更に前後のステップを[A-TRANS]則の適用によって結び付け る事で容易に構成できる．
証明終
部分型関係に関する図 2.2の規則群で\(*)" の付いていない公理と推論規則の中 で\(y)"が付けられている[S-WEAK]則はCardelli and Wegner (1985)に示された 本来の Funの規則群には存在しない．この推論規則は抽象型9 を固有の型構成子 として他の型構成子とは独立に導入している|本来の Funではそうしている| 場合には不要な規則である．しかし，定理 3.2 の証明での [S-EXIST] 則の導出や
[T-PACK]則の導出での(y)が付いているステップで見た通り，抽象型を独立な型構
成子として扱わずに多相型と関数型とでコード化する場合には，コード化で導入され る新しい型変数の処理の為に[S-WEAK]則が不可欠である．
同様に型付けに関する図2.3 の規則群で\(z)"が付された[T-TWEAK]則も本来 のFunには存在しないが，上の証明での[T-PACK]則の導出での(z)が付いている ステップでコード化で導入される型変数の処理の為に不可欠である．
注目すべき事は，抽象型を多相型と関数型とでコード化する場合の抽象型に関する 規則群の導出での[S-EXIST]則と[T-TWEAK]則との適用は，常に「自明な」適用 だという事である．即ち，これら二つの規則の適用で型変数の制約集合に追加される 新しい型変数に対する上限の型は常に最大の型Topである，という事実に注意する 必要がある．
2階命題論理での全称限量子8と含意とによる存在限量子9のコード化以来，
命題＝型 の立場から抽象型も多相型と関数型とでコード化可能と考えられ，また，
型のみならず対応する式構文に関しても正しく扱えると信じられて来た．しかし，束 縛型変数に対する範囲限定を許す場合には，コード化が全くの従来通りでは通用せず
新たに[S-EXIST] 則と[T-T-WEAK]則とを導入する必要がある，という事が，上
の定理の証明より判る．
基本的には以下に於いても抽象型は独立なものとして扱うが，抽象型を独立に扱う と繁雑になる場合には，以上の結果を用いて，抽象型は多相型と関数型とでコード化 されており抽象型に関する構文や推論規則は存在しないと看做し，抽象型を固有に扱 う事を省く場合がある．