Re: [心得] Dependent Type "簡"介 (離題)
針對epigram的心得
再來補充的詳細一點
順便騙點P幣來花花~ XD
※ 引述《noctem (noctem)》之銘言：
: ※ 引述《jaiyalas (ZZZ)》之銘言：
: : Epigram http://www.e-pig.org/
: : 據說有比較完整的dependent type
: : 也是我試最久卻最讓人動怒的東西..
: : 編輯上,實在是不太好用
: : 與其說是個editor,還不如說是一個"填空軟體"
: 哈哈哈...
: 其實如果 implement 得好，這是設計者 Conor McBride 心目中理想的
: 程式環境。你由定義 datatype 開始，然後 IDE 幫你找那個 datatype
: 的 induction 規則是什麼，程式會長什麼樣子，同時也確保程式會終止。
: 你就填空就可以了。
會繼續想說繼續用用看,一方面就是因為他的語法真的很有趣
另一方面也是因為我之前沒有用過這樣的方式在寫程式
所以也蠻好奇想要試看看寫起來是什麼感覺
先講他的優點好了,確實當我定義好function的signature以後
Epigrma會在另一塊buffer裡面告訴我哪裡該放怎樣的type
這點確實在對於對程式有相當程度瞭解的時候有幫助,
type會給予相當大的提示,但是,如果沒有那麼肯定的時候..
亂試亂試的,也根本不知道到底發生了什麼事情
誠如這個editor的undo功能所給人家的感覺。
寫這個editor的人似乎是覺得使用者都是可以
很順的從頭到尾寫下去而完全不會需要修改或是嘗試
另一個給人家這種感覺的地方是:
他的type資訊只有在function尚未定義完的時候會出現,
一旦結束了function的定義,就沒法再看type的資訊了
這對不是很熟悉他的作法的人來說,可能稍微增加了瞎子
摸象的程度。因為可能只是亂試試對了,但是還不清楚原因何在 (<-就是在說我 囧rz)
: （但我的感覺是，這跟 structure editor 不好用的原因一樣。它假設
: programmer 寫程式都很有條理、很有結構。但我寫程式都是塗塗抹抹的。）
說到塗塗抹抹,就一定要提一下epigram極其歡樂的undo
我一開始在看說明文件的時候還不太懂,為什麼會突然強調起undo這個話題
後來才知道,他的undo真是有夠難用 Orz
每undo一次,就會重新輸出整個buffer
這我不知道是不是xemacs的問題
但是我好幾次因為undo整個xemacs當掉
刷螢幕刷到程式當掉啦
其中好幾次還忘記存檔 囧rz
: 不過 epigram 只有他自己一個人在寫。聽說是關在房間裡面幾個月什麼
: 別的事情都不怎麼做... 因為只有一個人所以他選用他比較容易做出原型
: 的方式：寫成 emacs mode. 所以就變成這副模樣了。
這點真的相當讓人佩服
: 現在他正從 epigram 得到的許多經驗去構思 epigram 2. 聽說人手比較
: 多了，希望可以有人幫忙把這個界面的使用者經驗弄得好一點...
哦? :o
那真的會讓人期待一下
UI弄好的話,應該不會不好用的說
畢竟填空是個很方便的作法
: : 他另外有一個compiler
: : 但是難用程度不下於那個editor
: 好像真的很怒.. 辛苦啦..
沒有辛苦啦
這個根本沒有試出來 XD
裝的時候只是想說試試看
可以用就用一下看看,不能用就算了
結果光是安裝就讓我有被騙的感覺 XD
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 220.132.126.239
PLT 近期熱門文章
PTT數位生活區 即時熱門文章
