agda front-end design thoughts

Hi,

由於我的時間比較零碎一點，暫時還沒辦法很有系統地
閱讀現有程式，並思索是否有個周詳的設計方式。所以
想在這邊丟一點想法出來，看看大家是否有什麼想法？

現在 agda 是用 emacs 做 front-end, 如果要跳脫這個模式，
似乎是得重新設計 front-end 與 back-end 的協定。
現在 http 正大力（誤），因此第一個浮現在腦裡的，
也就是把這樣的協定做在 http 上。極端一點，
就可以有個 browser based agda front-end, 用 browser
寫 agda 之類的。就像很多 virtual private server 的廠商，
也有提供跑在 browser 上的 terminal, 讓你就好像用
ssh client 登入你的 virtual server 那樣。

另一方面，如果做在 http 上，我會希望可以做在 Hack 上：
這是模仿 ruby 的 rack, 而 ruby 的 rack 則是模仿 python 的 wsgi.

他大概的想法是，由於我們可能會有各種 http server,
也會有各種 web framework/application, 因此如果要讓
所有的後者跑在所有的前者上，直接溝通會導致產生
n * m 種組合。但如果中間有個 hack 做橋接，http server
針對 hack 來寫，web framework/application 也針對
hack 來寫，這樣頂多就只需要 n + m 種組合即可。

整個 http request 進入後端的流程大概會像這樣：

request -> happstack -> happstack hack handler ->
hack -> web framework adapter -> web application

因此畫成圖可能會長成這樣：

http server A -> A handler -> hack -> web framework C adapter -> ...
http server B -> B handler _/      \_ web framework D adapter -> ...

其中 handler 和 adapter 的部份，如果 http server 或
framework 直接支援的話，就不需要額外寫。
同時，hack 的介面非常單純，一個 Application 就是：

  type Application = Env -> IO Response

Env 裡面記錄了 query path, query string, request method 等資訊。
最笨的 hello world application, 不管 request 什麼，都回傳 hello world,
只要寫這樣：（from Hack readme）

  hello :: Application
  hello = \env -> return $ Response 
        { status  = 200
        , headers = [ ("Content-Type", "text/plain") ]
        , body    = pack "Hello World"
        }

另一個重要的元件，則是 Middleware, type 是：

  type Middleware = Application -> Application

middleware 希望做到的是，像是 design pattern 中的
decorator pattern, 透明地讓 middleware 成為 application 的
任意組件。例如計算 Content-Length 的 application,
可以透過串接而使得原本的 application 不需要做此計算，
只需要組合即可享有自動計算 Content-Length 的能力。

  content_length :: Middleware

他會從 target 中抽出 IO Response, 然後根據 body 計算 bytes,
再把 Content-Length 加到 headers 中，最後再吐出去。

於是我們只要做各種 Middleware 和 Application,
即可達到非常理想的模組化程度。

介紹大概到這..

如果把 agda front-end 做到上面，大概會長什麼樣子呢？
例如：

  POST /session/begin

這樣告訴 agda front-end 需要一個新的 session,
如果允許的話，就給予一個有效的 session cookie.

  Set-Cookie: agda-session=a-random-session-id

client 得知 session 開始後，就可以開始 parse 檔案：

  PUT /agda/parse
  Cookie: agda-session=a-random-session-id
  ...整個 agda 檔案內容

agda front-end 應該回傳什麼，需要看一下目前的資料格式...
後端的處理，或許大抵上可以這樣想：

1. 第一次收到 parse request 時，建立完整 parse tree

  data ParseTree = ...

2. 每一次 parse 完，建立完整資訊

  type ParseResult = (SourceCode, ParseTree)

3. 如果不是第一次 parse, 則做 delta parse

  source_diff :: SourceCode -> SourceCode -> SourceDiff
  parse_delta :: ParseResult -> SourceDiff -> ParseResult

第一個 ParseResult 是上一次的 parse 結果，
藉此只針對有變動的部份做 parsing.

  parse_delta previousResult
              (source_diff (fst previousResult) client_input)

不想玩時，則叫 agda front-end 釋放資源：

  POST /session/end

目前還沒細看 agda source code, 大概想到這裡。
有什麼想法嗎？