TaPL 読書会 15. Subtyping

8FE !EBJNBU[ 5B1-ಡॻձ 4VCUZQJOH

ࣗݾ঺հ ‣ !EBJNBU[ দຊେհ ౦ژ޻ۀେֶ େֶӃ৘ใཧ޻ֶݚڀՊܭࢉ޻ֶઐ߈ ઐ໳͸
ओʹϥϜμܭࢉϕʔεͷ ݴޠཧ࿦ w ଔ࿦Ͱ͸1SPMPHͰܕਪ࿦Λ࡞ͬͯ·ͨ͠ ϫʔΫεΞϓϦέʔγϣϯζͰόΠτ )BTLFMM 2

4VCUZQJOH ‣ 4VCUZQJOH ෦෼ܕ Λಋೖͨ͠ ୯७ܕʹର͢Δ֦ு ΦϒδΣΫτࢦ޲ 3
<: !

4VCUZQJOHͷ໨త ‣ Ͱ͸خ͘͠ͳ͍ྫ Ͱ͸5"QQΑΓԾҾ਺Sͷܕ͸Ͱͳ͍ ͱ͍͚ͳ͍͕ɺ࣮Ҿ਺ͷܕ͸ ͔͠͠SͷܕͰ͸ϑΟʔϧυYʹ੍͔͠໿͕ͳ͘ɺͦͷଞ ͷϑΟʔϧυ͕ͲΜͳܕͰ͋ͬͯ΋Τϥʔ͸ى͜Βͳ͍
͜ͷΑ͏ͳ߲΋ड͚෇͚͍͍ͯͷͰ͸ʁ 4 ! ( r : { x : Nat } .r.x ) { x = 0 , y = 1} ! r : { x : Nat } r : { x : Nat, y : Nat }

4VCUZQF ‣ ͱॻ͍ͯɺʮ4͕5ͷ4VCUZQFͰ͋Δʯͱఆٛ 5 S <: T

4VCUZQF3FMBUJPO 6 ` t : S S <: T `
t : T (T-Sub) S <: S (T-Refl) S <: U U <: T S <: T (T-Refl) ‣ 54VC͸5ZQJOH3FMBUJPOͱ4VCUZQF3FMBUJPOؒͷௐ੔ ઌͷྫͰ͸ ‣ ൓ࣹ཯ͱਪҠ཯Λຬͨ͢ ` { x = 0 , y = 1} : { x : Nat }

4VCUZQF3FMBUJPO SFDPSE ‣ 43DE8JEUIͱ43DE%FQUI͸ී௨ͷΦϒδΣΫτࢦ޲Ͱ ߟ͑Ε͹௚ײతʹ͸໌Β͔ ͦͯ͜͠ΕͰ5ZQF4BGFͰ͋Δ ‣ 43DE1FSN͸ʮϑΟʔϧυͷॱংͷҧ͍͸5ZQF4BGFUZʹ ͸Өڹ͠ͳ͍ʯ͜ͱΛද͢ 7
{li : Ti21..n+k i } <: {li : Ti21..n i } (S-RcdWidth) {kj : Tj21..n j } is a permutation of {li : Ti21..n i } {kj : Tj21..n j } < : {li : Ti21..n i } ( S-RcdPerm ) for each i [ Si < : Ti] {li : Si21..n i } < : {li : Ti21..n i } ( S-RcdDepth )

4VCUZQF3FMBUJPO GVODUJPO ‣ Ҿ਺͸ٯͷॱ൪ɺ໭Γ஋͸ಉ͡ॱ൪ Ͱ͋ΓͰͳ͍ܕʹ͍ͭͯ Ͱ͋Δؔ਺Λߟ͑Δͱ ͔ͭͷͱ͖ w
߲ʹTVCUZQFSFMBUJPO͸ͳ͍ͷͰਖ਼͍͠ॻ͖ํͰ͸ͳ͍ 8 T1 <: S1 S2 <: T2 S1 ! S2 <: T1 ! T2 ( S-Arrow ) R2 <: R1 R1 <: R2 R1, R2 f1 : R1 ! R2, f2 : R2 ! R1 f1, f2 R1 ! R2 <: R2 ! R1 r1 >: r2 f1(r1) <: f2(r2) f1 <: f2

1SPQFSUJFT ‣ 1SPHSFTTͱ1SFTFSWBUJPOΛյ͞ͳ͍Α͏ʹ஫ҙਂ͘ܕମܥ Λ֦ுͨ͠ɻ࣮ࡍʹյΕ͍ͯͳ͍͜ͱΛ֬ೝ͢Δɻ 9

1SPQFSUJFT ‣ -FNNB4VCUZQF3FMBUJPOͷٯ ͳΒ͹ ͳΒ͹4͸গͳ͘ͱ΋ʹ͍ͭͯ ͷܗ ͭ·Γ Ͱ͋Γɺ
Ͱ͋Δ֤ϥϕϧʹ͍ͭͯ 10 S <: T1 ! T2 S ⌘ S1 ! S2 S <: {li : Ti21..n i }

1SPQFSUJFT ‣ -FNNB ͳΒ͹͔ͭ ͳΒ͹ ͔ͭɺͰ͋ΔΑ͏ͳʹର͠ w ূ໌ɿTUSBJHIUGPSXBSEͳJOEVDUJPO
11 ` x : S1.s2 : T1 ! T2 T1 <: S1 , x : S1 ` s2 : T2 ` {ka = sain1..m a } : {li : Ti21..n i } {li21..n i } ✓ {ka21..m a } ka = li a, i ` sa : Ti

1SPQFSUJFT ‣ -FNNB4VCTUJUVUJPO ͔ͭͳΒ͹ w ূ໌ɿܕͷಋग़ʹؔ͢Δ*OEVDUJPO ‣ 5IFPSFN1SFTFSWBUJPO
͔ͭͳΒ͹ w ূ໌ɿܕͷಋग़ʹؔ͢ΔTUSBJHIUGPSXBSEͳJOEVDUJPO 12 , x : S ` t : T ` s : S ` [ x 7! s ] t : T ` t : T t ! t0 ` t0 : T

1SPQFSUJFT ‣ -FNNB$BOPOJDBM'PSN ͕ʹܕ෇͚͞ΕͨWBMVFͳΒɺ͸ͷܗ ͕ʹܕ෇͚͞ΕͨWBMVFͳΒɺ͸ ͷܗ ͨͩ͠ ‣
5IFPSFN1SPHSFTT ͕XFMMUZQFEͰDMPTFEͳWBMVFͳΒ͹ɺ͸WBMVF ΋͘͠͸Λຬ͕ͨ͢ଘࡏ͢Δ w ূ໌ɿܕͷಋग़ʹؔ͢ΔTUSBJHIUGPSXBSEͳJOEVDUJPO 13 v T1 ! T2 v x : S1.t2 v {li : Ti21..n i } v {kj = vj21..m j } {li21..n i } ✓ {ka21..m a } t t t ! t0 t0

5PQܕͱ#PUܕ ‣ ߏจͷ֦ு ‣ ܕ෇͚نଇͷ֦ு 14 T ::= ... types:
Top maximum type Bot minimum type S < : Top ( S-Top ) Bot < : T ( S-Bot )

5PQܕ ‣ 5PQܕ͸͢΂ͯͷܕͷ4VQFSUZQF +BWBͰ͍͏0CKFDUΫϥε ͢΂ͯͷ߲͸͜ͷܕʹͳΕΔ 4VCUZQJOHͱ1BSBNFUSJD1PMZNPSQIJTNΛ૊Έ߹Θͤ ͨγεςϜΛߏங͢Δͷʹ໾ཱͭ
w ষɾষͷ4ZTUFN' 15

#PUܕ ‣ #PUܕ͸͢΂ͯͷܕͷ4VCUZQF +BWBͰ͍͏OVMMͷܕ ΋͘͠͸Ϋϥε ͜ͷܕͷ߲͸ͲΜͳܕʹͰ΋ͳΕΔ DMPTFEWBMVFΛ࣋ͨͳ͍ͷͰɺWBMVFΛฦ͞ͳ͍Α͏ͳૢ࡞
ͷܕʹར༻Ͱ͖Δ w WBMVFΛฦ͞ͳ͍͜ͱΛϓϩάϥϚʹ௨஌͢Δ w ͍͔ͳΔWBMVFͷܕ͕ظ଴͞Ε͍ͯΔίϯςΩετͰ΋ͦ ͷܕΛ҆શʹར༻Ͱ͖Δ͜ͱΛ5ZQF$IFDLFSʹ௨஌͢Δ w ͋͘·Ͱܕ҆શੑͷ࿩ 16

#PUܕ ‣ ͔͠͠#PUܕʹΑͬͯ5ZQF$IFDLFS͕ෳࡶʹͳͬͯ͠· ͏ #PUܕ͕ͳ͍৔߹ɿ͕XFMMUZQFEͳΒ͸ؔ਺ܕ #PUܕ͕͋Δ৔߹ɿ͕XFMMUZQFEͳΒ͸ؔ਺ܕ ΋͘͠͸#PUܕ
/VMM1PJOUFS&YDFQUJPO )PBSFʮܕ҆શੑͷͨΊʹOVMMͷ֓೦Λߟ͕͑ͨɺ೥ؒ Ͱԯυϧن໛ͷաͪͩͬͨʯ ೥ 17 t1 t2 t1 t1 t2 t1

4VCUZQJOHBOE 0UIFS'FBUVSFT ‣ ʹϦετɺࢀরɺόϦΞϯτ౳ͷ֦ுΛೖΕ͍ͯ͘ 18 <:

"TDSJQUJPOͱ$BTUJOH ‣ 4VCUZQJOHͳ͠ͷ৔߹͸ධՁʹ͸ԿͷӨڹ΋ٴ΅ͣ͞ɺ୯ʹ ಡΈ΍͢͞Λਤͬͨ΋ͷͩͬͨ ‣ 4VCUZQJOH͋ΓͰ͸Ωϟετͷ໾ׂΛՌͨ͢ VQDBTUͱEPXODBTU ‣ VQDBTUͰ͸Uʹຊདྷਪଌ͞ΕΔܕͷTVQFSUZQFΛ͚ͭΔ
19 ` t : T ` t as T : T (T-Ascribe) . . . ` t : T . . . S <: T ` t : T T-Sub ` t as T : T T-Ascribe

"TDSJQUJPOͱ$BTUJOH ‣ EPXODBTUͰ͸ຊདྷਪଌ͞ΕΔܕͷTVCUZQFʹΩϟετ͢Δ EPXODBTU͕ਖ਼͘͠ߦΘΕ͍ͯΔ͔͸੩తʹղੳͰ͖ͳ͍ ‣ EPXODBTUΛೝΊΔͨΊͷنଇ ԿΒ͔ͷܕʹܕ෇͚Ͱ͖ΔͳΒͲΜͳܕʹͰ΋ܕ෇͚Ͱ͖Δ ‣
EPXODBTU͕ਖ਼͘͠ߦΘΕ͍ͯΔ͔͸࣮ߦ࣌ʹνΣοΫ͢Δ 20 ` t1 : S ` t1 as T : T ( T-Downcast ) ` v1 : T v1 as T ! v1 ( E-Downcast )

EPXODBTUͷྫ ‣ ͲΜͳܕͷҾ਺Ͱ΋ͦΕΛEPXODBTUͯ͠࢖͏ؔ਺ Λద༻͢Δͱ੒ޭ͢Δɻ ͷΑ͏ʹܕ෇͚͞ΕΔ Λద༻͢Δͱࣦഊͯ͠TUVDLʹؕΔ ‣ ͜͜·Ͱͷ֦ுͰͷQSFTFSWBUJPO͸อͨΕ͍ͯΔ͕ɺ
QSPHSFTTͷੑ࣭͸ࣦͬͯ͠·ͬͨ ྫ֎Λಋೖ͢Δ͔ɺEPXODBTUΛಈతͳܕνΣοΫͰஔ ͖׵͑Ε͹QSPHSFTTΛճ෮Ͱ͖Δ ԋश 21 f = ( x : Top ) ( x as { a : Nat }) .a ; {a = 5, b = true} ` v1 : T v1 as T ! v1 ( E-Downcast ) {a = 5, b = true} : {a : Nat} {b = true} <:

7BSJBOUT ‣ όϦΞϯτܕ TJNQMZUZQFEͷମܥͰ͸BTͰܕΛ໌ࣔ͠ͳͯ͘͸͍͚ͳ ͔ͬͨ UZQFVOJRVFOFTT͕յΕΔͱ͍͏࿩ ‣ ʹόϦΞϯτܕΛಋೖ͢ΔɻTVCUZQJOHͰʮॱ൪Λແ ࢹʯ͢Δ͜ͱʹΑΓɺܕͷ໌ࣔΛ͠ͳͯ͘ࡁΉΑ͏ʹͳͬͨ
22 < li : Ti21..n i > <:

7BSJBOUT 23

-JTUT ‣ -JTUίϯετϥΫλ͸DPWBSJBOU 24

3FGFSFODF ‣ ࢀরʹؔͯ͠͸ ‣ 4ͱ5͕lFRVJWBMFOUzͰ͋Δඞཁ͕͋Δ ͳͥͳΒࢀর͸ಡΈࠐΈઌ ͱͯ͠΋ॻ͖ࠐΈઌ
ͱ ͯ͠΋࢖ΘΕΔ͔Β 25

"SSBZ ‣ ഑ྻ͸ࢀর͕ͨ͘͞ΜฒΜͩΑ͏ͳ΋ͷ 26

3FGFSFODF"HBJO ‣ 3FZOPMET͸4PVSDFͱ4JOLͱ͍͏ίϯετϥΫλΛ༻͍ͯ ΑΓ༏Εͨࢀরͷܕ෇͚ΛఏҊͨ͠ 4PVSDF5͸5ܕͷಡΈࠐΈઐ༻ɺ 4JOL5͸5ܕͷॻ͖ࠐΈઐ༻ 27

3FGFSFODF"HBJO ‣ 4͕5ͷTVCUZQFͳΒɺࢀরηϧ͔ΒಡΈͩͨ͠஋͕ 4͕ܕͰ͋ΔݶΓͦΕΛ5ܕʹlEPXOHSBEFzͰ͖Δɻ ͭ·Γ4PVSDF͸DPWBSJBOU ‣ ٯʹ4͕5ͷTVQFSUZQFͳΒɺ4ܕͷࢀরηϧʹ ʮΑΓখ͍͞ʯܕͰ͋Δ5ܕͷ஋Λॻ͖ࠐΊΔ
ͭ·Γ4JOL͸DPOUSBWBSJBOU 28

3FGFSFODF"HBJO ‣ ࠷ޙʹ͜Ε·Ͱͷ3FGͰಡΈॻ͖Ͱ͖ΔΑ͏ɺ3FGΛ 4PVSDFͱ4JOLΛlEPXOHSBEFzͨ͠΋ͷͱ͢Δ 29

$IBOOFMT ‣ $IBOOFMUZQFT SFDFOUDPODVSSFOUQSPHSBNNJOHMBOHVBHF1JDU ܕͷ࿩Ͱ͍͏ͱɺDPNNVOJDBUJPODIBOOFM͕ࢀরηϧͷ Α͏ʹৼΔ෣͏ ‣ ਖ਼௚Α͘Θ͔ΒΜ͔ͬͨ
ɾТɾA 30

#BTF5ZQFT ‣ ΋ͬͱ͍Ζ͍ΖͳCBTFUZQF͕͋Δͱ͖͸ɺ ͷΑ͏ͳنଇ͕͋Δͱ ͷ͔ΘΓʹ ͱॻ͚Δɻ ৚݅෼ذͷ਺ΛݮΒͤͯศར ͳ͜ͱ΋͋Δ 31

$PFSDJPO4FNBOUJDT ‣ TVCUZQJOHʹΑͬͯ͡ΑΓॊೈͳܕ෇͚͕ՄೳʹͳΔͱड़΂ ͖͕ͯͨɺҙຯతͳ໘ʹ͍ͭͯ͸ৄ͘͠৮Εͯདྷͳ͔ͬͨ ‣ ࠓ·Ͱड़΂͖ͯͨΑ͏ͳࣜͷධՁํ๏͸୯७ͰΘ͔Γ΍͍͢ ΋ͷ͕ͩͬͨɺޮ཰ͷྑ͍΋ͷͰ͸ͳ͍ ಛʹ਺஋ԋࢉͱϨίʔυͷϑΟʔϧυ΁ͷΞΫηε ‣
͜Ε͔ΒTVCUZQJOHΛؚΉݴޠʹผͷҙຯΛ༩͑Δ DPFSDJPOTFNBOUJDTʹ͍ͭͯड़΂Δ DPFSDJPOڧ੍ʀ཈ѹɺҖѹʀ஄ѹ੓࣏ 32

4VCTFU4FNBOUJDTͷ໰୊ ‣ *OU'MPBUͳͲ͕͋Δͱɺ JOU5P'MPBU ͱ͔ॻ͔ͳ ͖Ό͍͚ͳ͍ͱ͜ΖΛ ͱॻ͚ΔΑ͏ʹͳΔͳͲศར ‣ ͔͠͠*OUͱ'MPBU͸ϝϞϦදݱ͕ҟͳΔͷͰɺ໌ࣔతͳ
DBTUΛল͘ͱ࣮ߦ࣌ʹPQFSBOEͷܕΛνΣοΫͯ͠ద੾ʹ JOU5P'MPBUΛೖΕΔ͜ͱ͕ඞཁʹͳΔ ‣ ϨίʔυͷϑΟʔϧυΞΫηεʹ͍ͭͯ΋ɺTVCUZQJOH͕ͳ ͚Ε͹ϑΟʔϧυͷ഑ஔ͸੩తʹܾ·͍ͬͯͨ ‣ TVCUZQJOHΛೖΕͨ͜ͱͰϑΟʔϧυͷॱ൪Λม͑ͯ΋Α͘ ͳΓɺϑΟʔϧυΞΫηε͸࣮ߦ࣌ʹઌ಄͔Βॱ࣍νΣοΫ ͍͔ͯ͠ͳ͚Ε͹ͳΒͳ͍ ‣ ͜ΕΒ͸࣮ߦ࣌ͷύϑΥʔϚϯε௿Լʹͭͳ͕Δ 33

$PFSDJPO4FNBOUJDT ‣ Ҏ্ͷ໰୊͸ผͷTFNBOUJDTΛ༻͍Δ͜ͱͰղܾ͢Δ TVCUZQJOHΛSVOUJNFDPFSDJPOʹΑͬͯऔΓڈΔ w *OUܕͱ'MPBUܕͷ଍͠ࢉ͸ʮ'MPBUܕʹἧ͑ͯ଍͢ʯ w Ϩίʔυ͸ฒͼΛҰఆʹ͔ͯ͠ΒΞΫηε ‣
͋ΔݴޠͷDPFSDJPOTFNBOUJDT͸ɺΑΓ௿Ϩϕϧͳݴޠ΁ ͷม׵ͱͯ͠දݱ͞ΕΔ ͜͜Ͱ͸͔ΒʹϨίʔυͱ6OJUܕΛՃ͑ͨ΋ͷ 34

$PFSDJPO4FNBOUJDT ‣ ݩͷ߲ͷͲͷ෦෼Ͱม׵͕ى͔ͬͨ͜Λ஌Δඞཁ͕͋Δ ݩͷ߲ͷಋग़໦ΛݟΕ͹Θ͔Δ ม׵ΛఆࣜԽ͢Δʹ͸ɺͦͷม׵Λܕنଇʹجͮؔ͘਺ ͷಋग़໦Λऔͬͯ 6OJU SFDPSEͷ߲Λฦ͢
Λ ߟ͑Δͷ͕ྑ͍ 35

$PFSDJPO4FNBOUJDT ‣ ܕͷͨΊͷؔ਺ ͷܕΛ 6OJU SFDPSEͷܕʹม׵͢Δ 5PQΛ6OJUʹม׵͢Δ͚ͩ 36

$PFSDJPO4FNBOUJDT ‣ Ͱʮ$͸45Λ݁࿦ͱ͢Δಋग़໦Ͱ͋ΔʯΛද͢ ‣ TVCUZQJOHͷͨΊͷؔ਺ 45ͷಋग़໦Λड͚औΓɺʮܕͷ߲Λड͚औΓܕͷ ߲Λฦؔ͢਺ʯΛฦ͢ 37

$PFSDJPO4FNBOUJDT ‣ Ͱʮ%͸ͷಋग़໦Ͱ͋ΔʯΛද͢ ‣ ໨తͷؔ਺ ͷಋग़໦Λड͚औΓɺܕͷ߲Λฦ͢ 38

$PFSDJPO4FNBOUJDT ‣ -FNNBͳΒ͹ ূ໌ɿ$ʹؔ͢Δؼೲ๏ ‣ 5IFPSFNͳΒ͹ ͨͩ͠͸͔ͭͷΑ͏ʹఆ ٛ͞ΕΔ
ূ໌ɿ%ʹؔ͢Δؼೲ๏ ‣ Ҏ্ͷΑ͏ʹDPFSDJPOTFNBOUJDTΛఆٛ͢Ε͹ɺ΋͏ ͷධՁنଇΛ࢖͏ඞཁ͸ͳ͘ɺม׵ޙͷ 6OJU SFDPSE ͷධՁنଇΛ࢖͏͜ͱ͕Ͱ͖Δ 39

$PIFSFODF ‣ DPFSDJPOTFNBOUJDTΛ༩͑Δࡍʹ஫ҙ͢΂͖͜ͱ͕͋Δ ‣ ྫ͑͹#BTFUZQFͱͯ͠*OU #PPM 'MPBU 4USJOH͕͋ΔݴޠͰ ͷΑ͏ͳTFNBOUJDTΛఆٛ͢ΔɻJOU5P4USJOH
zz qPBU5P4USJOH zzͩͱ͢Δͱɺ ͷධՁͷࡍ#PPM*OU4USJOHͱ#PPM'MPBU4USJOHͷ ͭͷϧʔτ͕ߟ͑ΒΕɺ݁Ռ͕ҧͬͯ͠·͏ lzͱlz 40

$PIFSFODF ‣ ͦ͜ͰDPFSDJPOTFNBOUJDTʹ͍ͭͯDPIFSFODFͱ͍͏ੑ ࣭Λߟ͑Δ ‣ %FpOJUJPO͋Δݴޠͷܕ෇͚ಋग़໦͔Βผͷݴޠ΁ͷ UFSN΁ͷม׵͕DPIFSFOUͰ͋Δͱ͸ɺม׵ݩͷݴޠͷ ೚ҙͷܕ෇͚ʹؔ͢Δ೚ҙͷಋग़໦ʹ͍ͭ ͯɺม׵ઌͷݴޠʹ͓͍ͯͱͷධՁ݁Ռ͕౳͍͠ ͜ͱΛ͍͏ɻ
‣ લͷεϥΠυͰड़΂ͨTFNBOUJDTʹ͍ͭͯ΋ɺ JOU5P4USJOH zz qPBU5P4USJOH zzͩͱ͢Ε͹ DPIFSFOUͰ͋Δɻ ΋ͬͱෳࡶͳݴޠؒʹ͓͍ͯDPIFSFODFΛอͭͷ͸େม 41

*OUFSTFDUJPOͱ6OJPO ‣ ܕͷؒʹJOUFSTFDUJPOͷԋࢉΛೖΕΔͱ΋ͬͱ༏Εͨ TVCUZQFؔ܎ΛಘΒΕΔɻ ‣ ܕͷ߲͸ʹ΋ʹ΋ܕ෇͚Ͱ͖Δ ‣ ͢ΔͱҎԼͷͭͷنଇ͸௚ײత 42

*OUFSTFDUJPOͱ6OJPO ‣ JOUFSTFDUJPOUZQFT͸ڧ͍ੑ࣭Λ࣋ͪɺ JOUFSTFDUJPO UZQFTʹ͓͍ͯܕ෇͚Ͱ͖Δ߲͸ਖ਼نԽ͞Ε߲ͨͰ͋Γɺͦͷ ٯ΋੒Γཱͭɻ ‣ UZQFSFDPOTUSVDUJPOQSPCMFN ষ ͕ඇܾఆతͰ͋Δ͜ͱ
Λࣔ͢ ‣ *OUFSTFDUJPOʹΑͬͯΦʔόʔϩʔυͷػೳ΋ఏڙ͢Δ ྫ͑͹ ͷΑ͏ͳԋࢉ͸*OUͷ଍͠ࢉʹ΋'MPBUͷ଍͠ࢉʹ΋࢖͑Δ ‣ ͔͠͠΋ͪΖΜJOUFSTFDUJPOUZQFTΛಋೖ͢Δ͜ͱͰ೉͍͠ ໰୊΋ੜͯ͡͠·͏ 43

*OUFSTFDUJPOͱ6OJPO ‣ VOJPOUZQF͸͔ʹܕ෇͚Ͱ͖Δ͜ͱΛࣔ͢ όϦΞϯτͱ͸ҟͳΓɺͦΕͧΕͷܕʹλά͸෇͔ͳ͍ ‣ EJTKPJOUͱOPOEJTKPJOUͳVOJPOUZQFTͷҧ͍͸ɺޙऀͷܕ Λ࣋ͭ஋ʹରͯ͠DBTFจʹΑΔϚονϯά͕Ͱ͖ͳ͍͜ͱ ͜ͷΑ͏ͳܕͷ஋ʹରͯ͠͸྆ํͷܕʹͱͬͯҙຯͷ͋Δ
ԋࢉ͔͠Ͱ͖ͳ͍ 44

TaPL 読書会 15. Subtyping

TaPL 読書会 15. Subtyping

More Decks by daimatz

Other Decks in Science

Featured

Transcript