Upgrade to Pro
— share decks privately, control downloads, hide ads and more …
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
590
PPL2016-9-3
Agda による定式化された型推論器の拡張と改良
Kyoko KADOWAKI
March 08, 2016
Tweet
Share
Other Decks in Science
See All in Science
データマイニング - コミュニティ発見
trycycle
PRO
0
160
04_石井クンツ昌子_お茶の水女子大学理事_副学長_D_I社会実現へ向けて.pdf
sip3ristex
0
640
統計的因果探索: 背景知識とデータにより因果仮説を探索する
sshimizu2006
4
1k
mOrganic™ Holdings, LLC.
hyperlocalnetwork
0
110
Symfony Console Facelift
chalasr
2
470
コンピュータビジョンによるロボットの視覚と判断:宇宙空間での適応と課題
hf149
1
350
機械学習 - 授業概要
trycycle
PRO
0
250
Transport information Geometry: Current and Future II
lwc2017
0
210
How To Buy, Verified Venmo Accounts in 2025 This year
usaallshop68
4
320
データマイニング - ノードの中心性
trycycle
PRO
0
270
データベース01: データベースを使わない世界
trycycle
PRO
1
800
Hakonwa-Quaternion
hiranabe
1
130
Featured
See All Featured
Context Engineering - Making Every Token Count
addyosmani
5
180
The Web Performance Landscape in 2024 [PerfNow 2024]
tammyeverts
9
850
CSS Pre-Processors: Stylus, Less & Sass
bermonpainter
358
30k
Testing 201, or: Great Expectations
jmmastey
45
7.7k
Creating an realtime collaboration tool: Agile Flush - .NET Oxford
marcduiker
32
2.2k
Art, The Web, and Tiny UX
lynnandtonic
303
21k
Refactoring Trust on Your Teams (GOTO; Chicago 2020)
rmw
35
3.2k
Fight the Zombie Pattern Library - RWD Summit 2016
marcelosomers
234
17k
The Power of CSS Pseudo Elements
geoffreycrofte
79
6k
Building Better People: How to give real-time feedback that sticks.
wjessup
368
20k
Bash Introduction
62gerente
615
210k
The Invisible Side of Design
smashingmag
301
51k
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શੑͷূ໌ ܕ͕͔ͭͳ͍߹