[心得] Dependent Type "簡"介

[jaiyalas (ZZZ)]

來分享點心得吧~ \囧/
最近幾個月接觸的東西

順便看看能不能稍稍激起一點這個版的活力..

有錯煩請各位多指教~ 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
推 PsMonkey:低手路人幫推
推 timTan:Good  期待下一篇
推 noctem:辛苦啦～欸，後來 Agda 裝得起來嗎？
推 jaiyalas:有~windows上有裝起來,但是ubuntu每次抓到一半就說有
→ jaiyalas:error 不知道是怎麼回事,不過這幾天稍微多事一點,還沒時
→ jaiyalas:間去慢慢試看看可以怎麼辦..