[Agda] Review (1) with dependent type

學校的東西弄的有點煩

Ruby的東西也因為暫時有點原地踏步而有點膩了

看一下之前弄到一半的東西

選了其中一個卡最久的agda來玩一下

希望可以轉換一下心情.

Agda is a dependently typed programming language.

簡單來說, 在agda中value和type之間的界線

就像是同步率超過400%一樣的曖昧不明.

這就是說,舉一個頗為俗爛的例子

我們可以定義出一個具有某個性質的結構.

e.g. 

一個一般的List可以定義如下

    data List (A : Set) : Set where

        nil : List A 

        cons : A -> List A -> List A

而在agda裡面我們可以在這個結構定義上追加一個屬性"長度"

    data List (A : Set) : Nat -> Set where

        nil : List A zero

        cons : {m : Nat} -> (a : A) -> List A m -> List A (1+m)

這有什麼了不起的地方呢?

關鍵之處在於"長度"是一個 value

而定義本身是一個資料"結構",換句話說他是一個 type

在一般常見的語言裡面這兩個是相當井水不犯河水的東西

而在像是agda這種語言裡面,

我們可以將兩者混合在一起

做出像是上面那樣的List定義: 

"一個本身帶有自身長度訊息的List"

這樣有什麼用處呢?

我們可以藉由dependent type來幫助我們

在type check時就確定某些程式的性質

甚至我們可以藉此來討論某些程式的恆真性(套套邏輯? XD)

例如說,我們知道長度m的list cancat 一個長度n的list

不管兩個list的內容如何,我們知道最後產生出來的list長度一定是m+n

而今天我們因為長度這個資訊是包含在我們的type上面的

所以我們可以在compile的時候就去檢查是否正確

(嚴格來說是在type check的時候)

這對於我們在確訂成市馬的正確性上面有非常正面的幫助

不過這再繼續講下就變成在討論dependent type了

所以先忘記那回事

只要先記得現在是我們是處在一個

value和type之間的界線相當模糊的世界裡就好..

(to be continued)