[GTK2HS] Testing

今天早上終於考完我的期中考惹

其實沒什麼念

但是卻寫的蠻順的

感覺logic那些東西有碰有差 @@

阿,雖說還是有幾個地方的證明想不出來

扯遠了

總之晚上喬好pre-ProG的事以後

趁著大腦很累的時候玩了一下gtk2hs

compiler > ghc 6.8.2

package > gtk2hs 0.9.12.1

gtk > x11/gtk2 2.12.9

跑起來長做這樣..

不太好看的感覺 @@

但是也不算太醜啦

只是X11實在是有那麼點遲鈍

[GTK2HS] Install on Mac OS X

一時興起

灌了wxHaskell和gtk2hs來用

不過wxHaskell不知道為甚麼不能跑

我猜是某個東西的版本不對

不過我暫時也懶得去找問題了

也許哪天用Arch來灌灌看(?) 

有.空.的.話.啦... XD

回到正題

gtk2hs官方網站上的tutorial

不知道為啥是用一個叫做Glade的軟體當作開發環境

然後我試著去抓下來build

不過build到一半有問題然後就卡住了

看起來是我有少東西

但是,懶散如我

我另外去google一下有沒有其他的tutorial

果不其然,找到了這個 

一個gtk2hs的toturial

(不過後來我也在gtk2hs官網上看到一樣的helloworld sample囧)

簡單講一下helloworld的作法

首先create一個檔案:

    import Graphics.UI.Gtk
    main :: IO ()
    main = do
      initGUI
      window <- windowNew
      button <- buttonNew
      set window [ containerBorderWidth := 10,
                   containerChild := button ]
      set button [ buttonLabel := "Hello World"]
      onClicked button (putStrLn "Hello World")
      onDestroy window mainQuit
      widgetShowAll window
      mainGUI

然後用ghc compile一下

> ghc --make gtktry.hs -o hello

> ./hello

這樣就好了

因為是在mac os上

所以會開出X11來

有點醜,但是也只能忍耐了 T^T

題外話1

後來我用macport弄到了Glade3

不過暫時沒有意願去測

雖說看起好像還不錯用的說

(port好強呀,什麼都有Orz)

題外話2

據說有個叫做HOC的東西

(Haskell to Object-C binding)

顧名思義,可以連接haskell和object-c

然後據說可以藉此使用mac上的cocoa

不過,cocoa我完全不熟

(其實完全沒碰過沒用過)

所以只是隨口提一下 XD

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

[NOTE] Parallel Desktop

7KU0H-EV7UC-04LTU-GYZSM-IZ50Y

[QtRuby] Install On Mac OS 10.5

一直都想寫個CAPD的程式
來處理每天要紀錄的資料
甚至是管理每個月的回診紀錄和數值統計

原本就是考慮用
Cpp 或是 Ruby 當作 language
然後用 HTML 或是 GUI(Qt) 來做輸出
因緣際會最後是決定採用 QtRuby 這樣的 tool

不過一開始裝的時候鬼打牆的非常嚴重
和之前裝openCV的問題有點像
都是因為Mac OS都預設你是在Xcode上面develop
所以很多東西他都直接幫你弄成.Framework 

但這對我這個不用Xcode的來說根本是惡夢一場 

(好吧,我承認很大的原因是我和Xcode完全不熟) 

最後是參考這位同學的作法: 

http://friends.roodo.com/diary/showDiary/26582

其中有關 ccmake 的部份補充如下:

> cd qt4-qtruby-1.4.10

> ccmake .

接著會出現如下圖所示的東西

請圖中紅色的部份改成非framework的path

(上圖中我已經將需要改的地方改成我要的了)

上面的改好以後按 't' 進入進階選項

先把INSTALL_PREFIX改成\opt\local\

或是任何慣用的路徑

(原本可能是\usr\local\或是\opt\kde4\

但是這會造成某些lib沒法link)

接著往下翻好幾頁以後

把有關ruby的path改一下

我懶得去框顏色了

總之,是RUBY_INCLUDE_PATH和RUBY_LIBRARY這兩個PATH

改好以後就直接

> cmake .

> make

> sudo make install 

這樣理論上就是裝好了 :)

然後就可以照著上面那個blog文章裡面範例去run看看