Lock in $30 Savings on PRO—Offer Ends Soon! ⏳
Speaker Deck
Features
Speaker Deck
PRO
Sign in
Sign up for free
Search
Search
PPL2016-9-3
Search
Kyoko KADOWAKI
March 08, 2016
Science
0
610
PPL2016-9-3
Agda による定式化された型推論器の拡張と改良
Kyoko KADOWAKI
March 08, 2016
Tweet
Share
Other Decks in Science
See All in Science
Lean4による汎化誤差評価の形式化
milano0017
1
380
2025-05-31-pycon_italia
sofievl
0
110
Text-to-SQLの既存の評価指標を問い直す
gotalab555
1
140
データベース14: B+木 & ハッシュ索引
trycycle
PRO
0
560
風の力で振れ幅が大きくなる振り子!? 〜タコマナローズ橋はなぜ落ちたのか〜
syotasasaki593876
1
160
データから見る勝敗の法則 / The principle of victory discovered by science (open lecture in NSSU)
konakalab
1
240
力学系から見た現代的な機械学習
hanbao
3
3.6k
ランサムウェア対策にも考慮したVMware、Hyper-V、Azure、AWS間のリアルタイムレプリケーション「Zerto」を徹底解説
climbteam
0
180
Accelerating operator Sinkhorn iteration with overrelaxation
tasusu
0
120
Ignite の1年間の軌跡
ktombow
0
180
動的トリートメント・レジームを推定するDynTxRegimeパッケージ
saltcooky12
0
240
デジタルアーカイブの教育利用促進を目指したメタデータLOD基盤に関する研究 / Research on a Metadata LOD Platform for Promoting Educational Uses of Digital Archives
masao
0
130
Featured
See All Featured
Rails Girls Zürich Keynote
gr2m
95
14k
CSS Pre-Processors: Stylus, Less & Sass
bermonpainter
359
30k
Testing 201, or: Great Expectations
jmmastey
46
7.8k
How to train your dragon (web standard)
notwaldorf
97
6.4k
Rebuilding a faster, lazier Slack
samanthasiow
84
9.3k
GraphQLとの向き合い方2022年版
quramy
50
14k
Reflections from 52 weeks, 52 projects
jeffersonlam
355
21k
How GitHub (no longer) Works
holman
316
140k
The Pragmatic Product Professional
lauravandoore
37
7.1k
No one is an island. Learnings from fostering a developers community.
thoeni
21
3.5k
Java REST API Framework Comparison - PWX 2021
mraible
34
9k
The Cult of Friendly URLs
andyhume
79
6.7k
Transcript
Agda ʹΑΔఆࣜԽ͞Εͨܕਪ ثͷ֦ுͱվྑ ͓ͷਫঁࢠେֶɹ߳ࢠɹઙҪ݈Ұ
1͡Ίʹ •ݚڀ֓ཁ •ݚڀഎܠ •ຊݚڀͷߩݙ •ൃදͷྲྀΕ
ݚڀ֓ཁ w"HEBΛ༻͍ͯɺఆࣜԽ͞ΕͨܕਪثʹHFOFSJD QSPHSBNNJOHෆ੍ࣜͳͲͷςΫχοΫΛ༻ ͍ͯɺ࣮Λ؆໌ʹ͠ɺߏจͷ֦ுΛ؆୯ʹͨ͠ wHFOFSJDQSPHSBNNJOH wෆ੍ࣜ
Agda ʹ͍ͭͯ wґଘܕΛ༻͍Δ͜ͱͷͰ͖Δɺఆཧূ໌ࢧԉγες Ϝ͓Αͼϓϩάϥϛϯάݴޠ w)BTLFMMͳͲʹจ๏͕ࣅ͍ͯΔ
ґଘܕ(Dependent Types) wʹґଘ͢ΔܕΛͭ͘Δ͜ͱ͕Ͱ͖Δܕ wྫ7FDOܕ OJOUܕͷ ͕͞OͷϕΫτϧΛ ܕͷϨϕϧͰ දݱ͍ͯ͠Δ wྫ͑ɺ0$BNMͷϦετͰ͕͞ܕϨϕϧͰࢦ
ఆͰ͖ͳ͍ MFOHUIؔͳͲͰऔΓग़͢͜ͱ͕ඞཁ
ఆࣜԽ ೖྗʢܕແ͠ݴޠʣ ग़ྗʢܕ͖ݴޠʣ ܕਪ n = 1 let f x
= match x with 0 -> “zero” | _ -> “not zero” n : int n = 1 f : int -> string f x = match x with …
ܕ ఆࣜԽ ೖྗʢܕແ͠ݴޠʣ ग़ྗʢܕ͖ݴޠʣ ܕਪ n : int f :
int -> string
ܕ ఆࣜԽ ೖྗʢܕແ͠ݴޠʣ ग़ྗʢܕ͖ݴޠʣ ܕਪ n : int f :
int -> string ݕূػߏ νΣοΫ ᶃ
ఆࣜԽ ೖྗʢܕແ͠ݴޠʣ ग़ྗʢܕ͖ݴޠʣ ܕਪ ܕΛফڈ ܕແ͠ݴޠ ಉ͡Ͱ͋Δ͜ͱΛอূ͢Δ
ݚڀഎܠ wܕਪΛ͢ΔʹVOJpDBUJPOͷػߏ͕ඞཁ͕ͩɺ ී௨ʹ࣮͢Δͱมͷॻ͖͑ͳͲ͕ඞཁͰɺ "HEBͰͰ͖ͳ͍ wͦ͜Ͱ.D#SJEFܕมͷΛົʹཧ͢Δܗ ͰVOJpDBUJPOͷػߏΛQVSFGVODUJPOBMʹ࣮ݱͨ͠ w͜ΕʹΑΓɺ"HEBͰܕਪثΛͭ͘Δ͕ग़དྷ ͨ
ຊݚڀͷߩݙ w.D#SJEF͕ࣔͨ͠VOJpDBUJPOͷػߏ<.D#SJEF >Λ֦ு͠ɺ୯ ҰԽͰ͖͍ͯΔূ໌ฦ͢ܗͰఆࣜԽͨ͠ʢ11-ʣ w͜ͷVOJpDBUJPOͷػߏΛͱʹͯ͠ɺ"HEBͰఆࣜԽ͞Εͨܕਪث Λ࣮ͨ͠ʢ11-ʣ w͜ͷܕਪثʹෆ੍ࣜΛಋೖ͢Δ͜ͱͰܕมΛࢦఆ͢Δͷ Έͷ࣮ΑΓ؆୯ʹ࣮͢Δํ๏Λࣔ͠ɺͦΕΛܕنଇͷܗͰఆ ࣜԽͨ͠ wVOJpDBUJPOͷػߏΛHFOFSJDQSPHSBNNJOHʹΑΓҙͷܕʹ
֦ு͠ɺܕͷ֦ுΛ؆୯ʹͨ͠ wܕਪͷ݁ՌɺಘΒΕͨܕ͖߲͔ΒܕΛऔΓআ͘ͱݩͷ߲͕ಘ ΒΕΔ͜ͱূ໌ͨ͠ wܕਪͷ֦ுͷྫͱͯ͠ɺΛಋೖͨ͠
ࠓͷίϯςϯπ ͡Ίʹ VOJpDBUJPO ܕఆٛ HFOFSJDQSPHSBNNJOHͱෆ੍ࣜ ܕਪ ·ͱΊ
2 unification •McBrideʹΑΔख๏ •unificationͷఆࣜԽ
McBride ʹΑΔ unification ͷػߏ McBrideɺܕมΛ༗ݶू߹Ͱදݱ͢Δख๏Ͱఀࢭੑ͕໌ Β͔ͳ unificationΛ࣮ݱͨ͠ ܕН B B
B N ܕมͷू߹ ࠷େͰNݸ ༗ݶू߹ pOJUFTFU N
McBride ʹΑΔ unification ͷػߏ ܕН B JOU B
N N ܕมೖʹΑΓ۩ମԽʢ۩ମతͳܕʹͳΔʣՄೳੑ͕͋Δ
ܕUBˠ BˠB B B B ܕUBˠ BˠJOU B
JOU B
ܕUBˠ BˠB B B B ܕUBˠ BˠJOU B
JOU B VOJpDBUJPO BJOU B JOU B
ܕUBˠ BˠB B B B ܕUBˠ BˠJOU B
JOU B VOJpDBUJPO BJOU B JOU B ❌ ۩ମԽ͞ΕͨܕΛू߹͔Βআ
ܕUBˠ BˠB B B B ܕUBˠ BˠJOU B
JOU B VOJpDBUJPO BJOU B B Bˠ BˠJOU ܕมͷ͕͔֬ʹݮ͍ͬͯΔ
ܕUBˠ BˠB B B B ܕUBˠ BˠJOU B
JOU B VOJpDBUJPO BJOU B B Bˠ BˠJOU ܕมͷ͕͔֬ʹݮ͍ͬͯΔ ܕม͕۩ମԽ͞ΕΔͨͼʹɺ۩ମԽ͞Ε͍ͯͳ͍ܕมͷ ͕ͻͱͭݮΔ
ܕUBˠ BˠB B B B ܕUBˠ BˠJOU B
JOU B VOJpDBUJPO BJOU B B Bˠ BˠJOU ܕมͷ͕͔֬ʹݮ͍ͬͯΔ ܕม͕۩ମԽ͞ΕΔͨͼʹɺ۩ମԽ͞Ε͍ͯͳ͍ܕมͷ ͕ͻͱͭݮΔ ఀࢭੑ͕໌Β͔
unificationͷఆࣜԽ wઌ΄Ͳࣔͨ͠ख๏ͰɺVOJpDBUJPOΛ"HEB্Ͱ࣮Ͱ͖ͨ wܕਪثΛఆࣜԽ͢Δʹz͔֬ʹVOJGZ͞Ε͍ͯΔzূ໌ Λฦ͢͜ͱඞཁ ɹࣜʹ͢ΔͱTVCTUМUTVCTUМU ʮೖͨ͠ޙͷܕ͕͔֬ʹಉҰʯ wVOJpDBUJPOͷؔΛ֦ுͯ͠ɺ͜ͷূ໌Λฦ͢Α͏ʹ͠ ͨʢ11-ʣ
3 ܕఆٛ •ܕɺܕஅɺ߲ •ຊݚڀʹ͓͚Δಛघͳදݱ
ܕఆٛ ߲
ܕఆٛ ߲ N൪ͷܕม ؔܕ
ܕఆٛ ߲ ม ϥϜμந ؔద༻
ܕஅ ਪنଇ
ܕஅ ਪنଇ ʮܕڥϵͷͱͰɺ߲.ͷܕНʹͳΔʯ
ܕஅ ਪنଇ
ܕਪͷಛघͳදݱ ܕΛܭࢉͯ͠ग़ྗ͢ΔͨΊͷنଇ
ܕਪͷಛघͳදݱ ೖྗ ग़ྗ
ܕਪͷಛघͳදݱ ᶃ߲.ͱ ܕมΛ࠷େͰNݸͭܕڥϵ͕ೖྗ͞ΕΔ
ܕਪͷಛघͳදݱ ᶄ৽͍͠ܕม͕ܕਪதʹN``NݸׂΓͯΒΕΔ
ܕਪͷಛघͳදݱ ᶅܕมͷΛN`ݸ·ͰݮΒ͢ೖ͕ಘΒΕΔ
ܕਪͷಛघͳදݱ ᶇܕมͷ͕N`·ͰݮͬͨܕН͕ฦͬͯ͘Δ
unification ͷಛघͳදݱ ܕНͱНΛಉ͡ʹ͢Δ VOJGZ͢Δ ೖМΛಘΔ
unification ͷಛघͳදݱ ೖྗ ग़ྗ
unification ͷಛघͳදݱ ܕมΛ࠷େͰN``ݸ࣋ͭܕН ͱН ܕมΛN``ݸ͔ΒN`ݸ·ͰݮΒ͢ೖМʹΑͬͯ VOJpDBUJPO ୯ҰԽ ͞ΕΔ
4 generic programmingͱ ෆ੍ࣜ •generic programming •ෆ੍ࣜ
generic programming wී௨ܕΛίϯετϥΫλͰఆٛ͢Δ w͜ͷ߹ɺܕΛૢ࡞͢Δؔʹ͓͍ͯɺܕΛ࠶࣮͢Δͨ ͼʹύλʔϯϚονΛ࠶࣮͢Δඞཁ͕͋Δ wܕΛHFOFSJDʹੜ͢Δ͜ͱͰɺύλʔϯϚονͷ࠶࣮ Λආ͚ɺϢʔβ͕ࢦఆͨ͠ҙͷܕΛ࠶࣮ͳ͘ਪͰ͖ ΔΑ͏ʹͳΔ wຊݚڀͰɺ3FHVMBS</PPSUΒ >ΛݩʹHFOFSJDͳ
ܕΛ࣮ͨ͠
generic programming ͷߏจ $POT 'TU 4OE Λ૿͍ͨ͠ͱ͖ɺ ੵܕΛՃ͢Δඞཁ͕༗Δ
generic programming ͜ͷΑ͏ʹܕΛ૿ͯ͠ɺ VOJpDBUJPOܕʹؔ͢Δิͷ࣮Λมߋ͢Δඞཁ͕ͳ͍
generic programming ߏจΛ૿͢ͱ͖ɺ ߏจͦͷͷͷܕਪʹूதͰ͖Δ
generic programming ܕΛ#/'ͷΑ͏ͳܗͰදݱ͢Δ
generic programming ܕΛ#/'ͷΑ͏ͳܗͰදݱ͢Δ
generic programming ܕΛ#/'ͷΑ͏ͳܗͰදݱ͢Δ
generic programming ܕΛ#/'ͷΑ͏ͳܗͰදݱ͢Δ
generic programming ܕΛ#/'ͷΑ͏ͳܗͰදݱ͢Δ
generic programming ܕΛ#/'ͷΑ͏ͳܗͰදݱ͢Δ ͜ΕͰɺܕͷදݱ͕Ͱ͖ͨ
generic programming ۩ମతͳܕͷදݱ
generic programming දݱͷҙຯΛ༩͍͑ͯΔ
generic programming ࣗࣗΛ༩͑Δ͜ͱͰ࠶ؼ͢Δ
generic programming ࠶ؼΛด͡ΔͨΊͷܕ
generic programming ࠶ؼΛด͡ΔͨΊͷܕ
generic programming ࠶ؼΛด͡ΔͨΊͷܕ
generic programming ҙʹେ͖͍ܕΛදݱͰ͖Δ
ෆ੍ࣜ ܕਪΛ࣮͢ΔࡍɺҎલN``ΛݫີʹܕʹΈ ࠐΜͰ͍ͨ
ෆ੍ࣜ ͨͱ͑-BNTΛܕਪ͢Δͱ͖ N``/BU N``DPVOUT ϵ`$YUN`` ϵʜ
ෆ੍ࣜ ͨͱ͑-BNTΛܕਪ͢Δͱ͖ N``JOU N``DPVOUT ϵ`$YUN`` ϵʜ ܕͷϨϕϧͰܕΛ߹Θͤͯূ໌͠ͳ͍ͱ͍͚ͳ͘ͳΔ
ෆ੍ࣜ N``N≤N`Λຬ͍ͨͯ͠ΕΑ͘ɺ۩ମతͳ Ҏޙ࣋ͪา͘ඞཁ͕ͳ͍ ΘΓʹN≤N``ͱ͍͏ূ໌Λ࣋ͪา͘
5 ܕਪ • ؔఆٛ • ܕਪͷྫ - ؔద༻ -
ؔఆٛ ೖྗ TNݸͷܕมΛͭXFMMTDPQFEUFSN ϵܕڥ ग़ྗ N⒌⒌ N⒌ࣗવ N≤N⒌⒌N≤N⒌⒌Ͱ͋Δ͜ͱͷূ໌ МN⒌⒌ݸͷܕมΛ࣋ͭܕΛN⒌ݸͷܕมΛ࣋ͭܕʹ͢Δೖ Нਪ݁Ռͷܕ
Xਪ͞ΕͨXFMMUZQFEUFSNɻܕมΛN⒌ݸͭ FSBTFX㲇Tฦ͞ΕͨXFMMUZQFEUFSNT͔ΒܕใΛআͨ͠ͷ͕ɺ ͱͷXFMMTDPQFEUFSNͱ͍͠ͱ͍͏ূ໌ JOGFS
ؔఆٛ ೖྗ TNݸͷܕมΛͭXFMMTDPQFEUFSN ϵܕڥ .BZCF ग़ྗ N⒌⒌ N⒌ࣗવ N≤N⒌⒌N≤N⒌⒌Ͱ͋Δ͜ͱͷূ໌ МN⒌⒌ݸͷܕมΛ࣋ͭܕΛN⒌ݸͷܕมΛ࣋ͭܕʹ͢Δೖ
Нਪ݁Ռͷܕ Xਪ͞ΕͨXFMMUZQFEUFSNɻܕมΛN⒌ݸͭ FSBTFX㲇Tฦ͞ΕͨXFMMUZQFEUFSNT͔ΒܕใΛআͨ͠ͷ͕ɺ ͱͷXFMMTDPQFEUFSNͱ͍͠ͱ͍͏ূ໌ JOGFS
ؔఆٛ ೖྗ TNݸͷܕมΛͭXFMMTDPQFEUFSN ϵܕڥ .BZCF ग़ྗ N⒌⒌ N⒌ࣗવ N≤N⒌⒌N≤N⒌⒌Ͱ͋Δ͜ͱͷূ໌ МN⒌⒌ݸͷܕมΛ࣋ͭܕΛN⒌ݸͷܕมΛ࣋ͭܕʹ͢Δೖ
Нਪ݁Ռͷܕ Xਪ͞ΕͨXFMMUZQFEUFSNɻܕมΛN⒌ݸͭ FSBTFX㲇Tฦ͞ΕͨXFMMUZQFEUFSNT͔ΒܕใΛআͨ͠ͷ͕ɺ ͱͷXFMMTDPQFEUFSNͱ͍͠ͱ͍͏ূ໌ JOGFS OPUIJOH͕ฦΔܕΤϥʔͰ͋Δ
ؔఆٛ ίʔυͰ͜ͷΑ͏ʹͳΔʢࢀߟʣ
ܕਪͷྫ (App) "QQTTͷܕਪ TΛܕਪ͠ɺМͱНΛಘΔ ϵʹМΛࢪ্ͨ͠ͰTΛܕਪ͠ɺМͱНΛಘΔ ННˠЌ Ќ৽͍͠ܕม ͱͳΔΑ͏VOJGZ͠ ޭͨ͠ΒМΛಘΔ
ฦ͞ΕΔܕЌͱͳΔ
ܕਪͷྫ (App) "QQTTͷܕਪ TΛܕਪ͠ɺМͱНΛಘΔ ϵʹМΛࢪ্ͨ͠ͰTΛܕਪ͠ɺМͱНΛಘΔ ННˠЌ Ќ৽͍͠ܕม ͱͳΔΑ͏VOJGZ͠ ޭͨ͠ΒМΛಘΔ
ฦ͞ΕΔܕЌͱͳΔ
ܕਪͷྫ (App) "QQTTͷܕਪ TΛܕਪ͠ɺМͱНΛಘΔ ϵʹМΛࢪ্ͨ͠ͰTΛܕਪ͠ɺМͱНΛಘΔ ННˠЌ Ќ৽͍͠ܕม ͱͳΔΑ͏VOJGZ͠ ޭͨ͠ΒМΛಘΔ
ฦ͞ΕΔܕЌͱͳΔ
ܕਪͷྫ (App) "QQTTͷܕਪ TΛܕਪ͠ɺМͱНΛಘΔ ϵʹМΛࢪ্ͨ͠ͰTΛܕਪ͠ɺМͱНΛಘΔ ННˠЌ Ќ৽͍͠ܕม ͱͳΔΑ͏VOJGZ͠ ޭͨ͠ΒМΛಘΔ
ฦ͞ΕΔܕЌͱͳΔ
ܕਪͷྫ (App) TΛܕਪ͠ɺМͱНΛಘΔɻ ϵʹМΛࢪ্ͨ͠ͰTΛܕਪ͠ɺМͱНΛಘΔɻ
ܕਪͷྫ (App) TΛܕਪ͠ɺМͱНΛಘΔɻ ϵʹМΛࢪ্ͨ͠ͰTΛܕਪ͠ɺМͱНΛಘΔɻ
ܕਪͷྫ (App) TΛܕਪ͠ɺМͱНΛಘΔɻ ϵʹМΛࢪ্ͨ͠ͰTΛܕਪ͠ɺМͱНΛಘΔɻ
ܕਪͷྫ (App) ϵʹМΛࢪ্ͨ͠ͰTΛܕਪ͠ɺМͱНΛಘΔɻ ННˠЌ Ќ৽͍͠ܕม ͱͳΔΑ͏VOJGZ͠
ܕਪͷྫ (App) ϵʹМΛࢪ্ͨ͠ͰTΛܕਪ͠ɺМͱНΛಘΔɻ ННˠЌɹɹɹɹͱͳΔΑ͏VOJGZ͠ N`൪ͷܕมΛ৽͘͠औΓग़͢
ܕਪͷྫ (App) ННˠЌɹɹɹɹͱͳΔΑ͏VOJGZ͠ ޭͨ͠ΒМΛಘΔ
ܕਪͷྫ (App) ННˠЌɹɹɹɹͱͳΔΑ͏VOJGZ͠ ޭͨ͠ΒМΛಘΔ
ܕਪͷྫ (App) "QQͷܕنଇΛద༻͢Δɻ
"QQͷܕنଇΛద༻͢Δɻ
ܕਪͷྫ (App) "QQͷܕنଇΛద༻͢Δɻ ඞཁͳೖ
ܕਪͷྫ (App) "QQͷܕنଇΛద༻͢Δɻ ͳΔೖМΛฦ͍ͨ͠
ܕਪͷྫ (App) "QQͷܕنଇΛద༻͢Δɻ ͳΔೖМΛฦ͍ͨ͠
ܕਪͷྫ (App)
ܕਪͷྫ (App) ଞͷߏจ 'TU 4OEͳͲ ʹؔͯ͠ಉ༷ʹূ໌Ͱ͖Δ
·ͱΊ wܕมΛͰͳ͘ෆࣜΛ༻͍ͯදݱ͢Δํࣜʹ վྑ͠ɺ·ͨܕఆٛΛHFOFSJDQSPHSBNNJOHͷߟ ͑ํΛऔΓೖΕͯΑΓҰൠతʹվྑ͢Δ͜ͱͰɺܕ ਪثʹ͓͚ΔTZOUBYͷ֦ுͱূ໌ͷ؆ུԽΛ࣮ ݱͨ͠ wιʔείʔυHJUIVCDPNLEYVJOGFSBHEB "HEB߹ܭߦ
ࠓޙͷ՝ wߏจͷ֦ு ଟ૬ͷ-FUจͳͲ 1PMZ1<+BOTTPOΒ >*OEFYFE'VODUPST<-ÖIΒ >ͳͲܕύϥϝλΛѻ͑ΔͷΛ͏ඞཁ͕͋Δ wશੑͷূ໌ ܕ͕͔ͭͳ͍߹