[Agda] Instance Arguments

出來跑，遲早都要還的... XD

最近在試著使用 agda 裡面的 record，尤其是用來模擬 haskell 中的 type class。不過，用起來一直怪怪的，到處都綁手綁腳的。剛好前兩天看到 josh 的文章，裡面提到今年的 ICFP 有人在弄 type classes in agda。哪裡還有客氣的，趕快去找來看 XD。

大概看過去，看起來相當不錯的感覺，不過就是他沒有寫清楚實作上的細節。稍微查了一下發現 agda 號稱 2.2.12 就會有開始提供這個東西：
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArguments
也有講到如何用 instance argument 來做 type class：
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.ModellingTypeClassesWithInstanceArguments

不過不過，現在 stable agda 才 2.2.10；development version 也才不過 2.2.11！看來只好慢慢等了。

另外，agda 的 instance arguments 畢竟還是和 haskell 裡面的 type class 不一樣。type class 基本上會自動遞迴地去試圖找出一個 instance，但是 instance argument 設計上限制我們必須要真的給它一個 instance。老實說，這邊目前還不是了解，看看以後能不能多懂一點。附上參考資料：
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Non-recursiveResolutionForInstanceArguments

[agda] Review (2)

承接上一篇

這裡講解一個簡單的範例

第一步

我們先定義幾個基本且常見的東西

自然數(Nature Number)是一個type

一個自然數如果不是Zero就是某個自然數+1

    data Nat : Set where

        zero : Nat

        suc : Nat -> Nat

對某一個type A, List A n是A上面的一個長度為n的List結構

一個List如果不是空的(Nil)就是某一個元素接上另一個List

    data List {A : Set} : Nat -> Set where

        nil : List A zero

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

關於我們的資料結構就那兩個而已,非常簡單

然後下面我們來定義幾個常用的function

    _+_ : Nat -> Nat -> Nat

    zero + n = n

    (suc m) + n = suc (m + n)

    _++_ : {A : Set} -> {m n : Nat} -> 

                   List A m -> List A n -> List A (m+n)

    nil ++ xs = xs

    (cons x xs) ++ ys = Cons x (xs ++ ys)

前者是一般Nat在用的加法

後者是List在用的加法

"++"一般我們稱為 concat 或是 append

比較值得一提的是List A (m+n)這裡

我們知道m,n都是Nat, 而m+n也是一個Nat

問題在於,independent typed language中

我們是不能在type上做這樣operating的

例如說我們絕對不會看到

    (double + String) var = ?? ; 

這樣的東西出現在我們的java或是C++程式裡面

可是在agda中我們可以直接這樣做

這也就是上一篇中說得"value與type之間的曖昧不明"

再接下去下面的定義之前

我們先來看看目前為止我們可以做什麼?

more over, 有什麼好處?

(方便起見,這裡先用比較general的語法來表示)

假設我們現在有兩個List:

    a = [1,2,3]

    b = [4,5]

我們知道a, b兩者的type:

    a : List Nat 3  (長度3的整數list)

    b : List Nat 2  (長度3的整數list)

所以,我們可以想像出:

    a ++ b : List Nat 5

    a ++ b = [1,2,3,4,5]

這是非常理所當然的

我們腦海裡確實是這樣的結果

但是我們怎麼知道真正跑起來的時候 ++ 會是正確的?

或著說,我們希望能盡早確定這個function一定正確

那麼,最早,我們多早能確定呢? 

如果我們可以抽象且廣泛的描述這個function

(也就是定義這個function的同時)

而且知道它一定會正確的執行

那麼對於每一個實際執行時的case

它都絕對會是正確的

否則這段有問題的code根本不會通過type checking

更別提還要執行了

稍微回憶一下++的定義

我們根據++的type知道對於長度為m, n的list a, b

它都會正確的產生出一個長度是(m+n)的list

所以我們知道它在我們重視長度問題時一定是正確的

他不可能會在跑 [1,2,3] ++ [4,5,6] 時跑出一個長度不是6的list

因為List Nat 5和 List Nat 6根本是不同的type

(to be continued)

[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)

[Agda] 2.1.3 -Install

全程參照這一頁:
http://www.cs.chalmers.se/~ulfn/darcs/Agda2/README

使用的環境:
ubuntu-7.10
GHC-6.8.1

依序安裝下面的GHC package
binary-0.4.1
zlib-0.4.0.1 (部份linux要先安裝zlib1g-dev)
QuickCheck2.0
可以用"$ ghc-pkg -l"查詢現在已經有的pkg
可以去下列網站找所需要的
http://hackage.haskell.org/packages/archive/pkg-list.html

然後下載Agda..
一開始我是抓wiki上面的.tar.gz檔
但是build的時候一直說找不到"../../undefined.h"
後來是用darcs抓下來裝
(btw, darcs抓到的是2.1.3, 但是wiki上面只有2.1.2 .. =口=)
agda lib裝好以後
就把interpreter裝上去就結束了
詳情請參考readme檔

--
如果是GHC-6.1.1以前的版本
下面的lib都要用較早的版本
不然cabal不會過
binary-0.3
zlib-0.3 (部份linux要先安裝zlib1g-dev)
另外要幫GHC裝新版的src和mtl這兩個package
(QuickCheck的話我忘記有沒有要裝,舊版的agda好像不需要)
之後再裝agda即可