Re: [心得] Dependent Type "簡"介

看板PLT (程式語言與理論)作者noctem (noctem)時間17年前 (2007/10/01 15:50)推噓0(0推 0噓 0→)

留言0則, 0人參與討論串2/5 (看更多)

※ 引述《jaiyalas (ZZZ)》之銘言： : 據說,這個版的版主之前有嘗試過以這樣的方式來實做 : 也許可以請版主大人稍微講一下實做的心得 = =+ 嗯，我是證人。因為看不懂所以很快放棄了... XD : Haskell(GHC-6.6.1) : 最一開始使用的語言 : 不過因為他對於dependent type的支援不是很好 : ( 雖說好像有GADT,但是我不太知道那是什麼 : 也許哪個高手可以幫我補充一下,囧> ) : 沒試幾次以後就轉向其他語言了 GADT 是 Generalized Algebraic Datatype. 不過要解釋 generalized XYZ, 就得要先解釋 XYZ... 所以... 等到有觀眾要求再說好了... Haskell 其實還是沒有要做 dependent type 的意思。有人說 Haskell 近幾年（包括加入 GADT、日後可能有的type family 等等）的一連串擴充嘗試是往 dependent type 靠近的過程。但對於跨出這最後幾步，Haskell 似乎還是蠻遲疑的。畢竟大家對該怎麼做 dependent type 還是沒個共識，而且有了它之後，程式的風貌可能改很多，這也是大家所陌生的。 Dependent type 聽說倒是在 proof assistants 之中常用到。 GADT 好像就是學來的。 : Omega http://web.cecs.pdx.edu/~sheard/Omega/index.html : 沒有試過,只有看過程式碼 : 感覺語法和Haskell很像 : Epigram http://www.e-pig.org/ : 據說有比較完整的dependent type : 也是我試最久卻最讓人動怒的東西.. : 編輯上,實在是不太好用 : 與其說是個editor,還不如說是一個"填空軟體" 哈哈哈... 其實如果 implement 得好，這是設計者 Conor McBride 心目中理想的程式環境。你由定義 datatype 開始，然後 IDE 幫你找那個 datatype 的 induction 規則是什麼，程式會長什麼樣子，同時也確保程式會終止。你就填空就可以了。（但我的感覺是，這跟 structure editor 不好用的原因一樣。它假設 programmer 寫程式都很有條理、很有結構。但我寫程式都是塗塗抹抹的。）不過 epigram 只有他自己一個人在寫。聽說是關在房間裡面幾個月什麼別的事情都不怎麼做... 因為只有一個人所以他選用他比較容易做出原型的方式：寫成 emacs mode. 所以就變成這副模樣了。現在他正從 epigram 得到的許多經驗去構思 epigram 2. 聽說人手比較多了，希望可以有人幫忙把這個界面的使用者經驗弄得好一點... : 語言本身,實在是.. : 難以形容的詭異.. 嗯，這是一個有二度空間語法的語言. 用 - 和 | 等等符號畫格子。我很難想像它的 parser 怎麼寫的。 : 他另外有一個compiler : 但是難用程度不下於那個editor 好像真的很怒.. 辛苦啦.. : Agda2 http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php : 現在才要開始嘗試的東西 : 希望會比Epigram好用很多 Orz 我想至少是會比較習慣啦... BTW, Agda 本來也是在 proof assistant 裡面用的語言。 * * * 另外，還可以提一下越來越紅的 proof assistant: Coq. http://coq.inria.fr/ 基本概念上 Coq 也是用 Curry-Howard isomorphism 幫你做證明：一個 type 就是一個 proposition, 如果找得到一個有這種 type 的 term, 就是找到了一個該 proposition 的證明。為了描述更多想描述的 proposition, 使用 dependent type 就是蠻自然的事情。 Coq 等等 proof assistant 的使用經驗是使用者一直去和系統對話。當寫好一個證明（寫出一個 term）之後，Coq 可以 extract 出一個 OCaml 程式給你。（Coq 本身也是用 OCaml 寫的。Agda 則是 Haskell. 設計者的偏好也反應在這兩個語言的語法上... ） Agda 的 Emacs mode 也有一點對話的感覺，但已經比較像程式設計而不是定理證明。Epigram 是這種互動程式設計的新嘗試。像 Omega 的做法則是老 programmer 對新 tool 的抗拒 -- 回到老方法去，死也不改。 :) : 有哪位高手可以提供一點鍛鍊自己邏輯能力的方法.. : 最近覺得自己邏輯沒有學好 : 很多證明的東西常常沒法很快轉過來欸... 很多 computer scientist (指自己) 其實只會一種證明方法: 歸納法。大概多看多做就會了吧....? -- ※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 140.109.20.217