來分享點心得吧~ \囧/ 最近幾個月接觸的東西 順便看看能不能稍稍激起一點這個版的活力.. 有錯煩請各位多指教~ 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