[心得] Dependent Type "簡"介

看板PLT (程式語言與理論)作者jaiyalas (ZZZ)時間17年前 (2007/10/01 01:18)推噓4(4推 0噓 2→)

留言6則, 4人參與討論串1/5 (看更多)

來分享點心得吧~ \囧/ 最近幾個月接觸的東西順便看看能不能稍稍激起一點這個版的活力.. 有錯煩請各位多指教~ o(_ _)o ==前言分隔線== Type System Type System是一個Programming Language中很重要的一個部分它可以幫助我們把程式中的values和expressions給分類好 Type System可以檢查出我們程式的一些錯誤也可以幫助我們最佳化我們的程式舉例來說 > int i = 10; 這樣就是宣告變數i具有int的type 後面都用 i:int 這樣來表示variable及其所擁有的type 假設我們今天有個function:foo foo吃一個int,吐出另一個int > int foo(int i){ > return i + i; > } > > String v = foo(10); //error 如此一般,compiler會吐出一個error 告訴你 v 和 foo(10) 這兩個的type是不同的 v:String foo(10):int 這就是type system的功能之一它會幫我們做一些檢查 ====== 接著是讓人歡樂無限的Dependent Type \囧> 在真正講到dependent type之前回憶一下我們一開始的糖炒栗子 > int i = 10; 我們知道 i:int 也就是說,我們知道我們的資料(也就是i) 有一個叫做int的特性(屬性) 一個複雜一點的宣告可以告訴我們更多關於我們的資料的特性 > class List<E e>{ ... } > List<String> myList = new List<String>; class List<E e> 表示我們定義一個叫做List的class 這個class本身會需要一個"型別參數" 也就是說,我們可以在實體化List物件時寫 List<Integer>或List<String>之類的分別表示"裝Integer的List"和"裝String的List" 上面那樣的作法稱為generic programming(泛型) 不過,在這裡我們先不討論泛型的用法與意義 (這裡比我瞭解泛型的人應該是多到數不完,我還是不要丟臉好了XD) 不過必須一提的是,我們確實可以用這樣的方法來實做出dependent type 這點,希望在各位看官看完這篇文章以後,可以自行想像出來題外話一下據說,這個版的版主之前有嘗試過以這樣的方式來實做也許可以請版主大人稍微講一下實做的心得 = =+ 回到主題,上面程式片段第二行的意思就很明顯了一言以蔽之,就是 myList:List<String> 講的白話一點,我們知道我們的myList這個變數具有兩個特性 1)他是一個list 2)他不但是list,而且這個list裡面裝的所有資料的型態都是String 和上面那個陽春的 i:int (只單純的顯示了資料的種類) 來做比較我們現在的 myList:List<String> 不但顯示了資料結構,也顯示了資料內容物的型別回到我們一開始的名詞: dependent type 這個東西指就是"把資料的特性給建立進形別之中" dependent type - 相依(於資料)的形別這東西能做什麼呢?? 很簡單,他能擴充我們的type身上能裝載的特性我們可以把各個資料結構的特性給放進type裡面這對於checking和最佳化等等都有不錯的幫助例如說,我們可以把一個list的長度給放進type裡面 [1,2,3]和[1,2,3,4]這兩個list的type就會是不一樣的: [1,2,3] : List Integer 3 [1,2,3,4] : List Integer 4 而,如果我們把兩個list接起來新的list一定是某個type是List Integer 7的list 如果我們拿到的list的type不是這樣那就一定是有問題的,也許是有資料遺失或是重複了而不是在我們真的要用這個list的時候才發現不對勁小結論 \囧/ dependent type是用來強化我們工具的東西它會讓我們programming變的複雜且充滿限制而他確實的好處,其實只是讓我們程式提高"正確性" 以上,是我對dependent type粗淺的瞭解相信一定很多高手想要幫我補充請大家鞭小力點啦 >/////< ====== 實際上我在摸索上面那些東西的時候使用的工具不是java或是C++ 而是一些functional language 所以針對這個也做點"我所知道的介紹" 順便附上一點個人的感想 Haskell(GHC-6.6.1) 最一開始使用的語言不過因為他對於dependent type的支援不是很好 ( 雖說好像有GADT,但是我不太知道那是什麼也許哪個高手可以幫我補充一下,囧> ) 沒試幾次以後就轉向其他語言了 Omega http://web.cecs.pdx.edu/~sheard/Omega/index.html 沒有試過,只有看過程式碼感覺語法和Haskell很像 Epigram http://www.e-pig.org/ 據說有比較完整的dependent type 也是我試最久卻最讓人動怒的東西.. 他是個editor-typechecker-interpreter的綜合體編輯上,實在是不太好用 undo的時候容易當掉存檔讀檔也都很麻煩與其說是個editor,還不如說是一個"填空軟體" 語言本身,實在是.. 難以形容的詭異.. 有興趣的人可以去下載example來看.. 他另外有一個compiler 但是難用程度不下於那個editor 網站上的說明和下載下來的不一樣 http://www.dcs.st-and.ac.uk/~eb/esc.php Agda2 http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php 現在才要開始嘗試的東西希望會比Epigram好用很多 Orz (謎之聲:話說我一開始是想寫agda,怎麼反而這個講最少?? XD) ======以下是順便問問題區有哪位高手可以提供一點鍛鍊自己邏輯能力的方法.. 最近覺得自己邏輯沒有學好很多證明的東西常常沒法很快轉過來但是,對於要怎麼學好,我實在是沒有個概念 @"@ 以上,謝謝 o(_ _)o -- ※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 220.132.126.239