Example Chu2 Application in Agda
module Hello where
open import IO.Primitive using (IO; return)
open import Foreign.Haskell using (Unit)
open import Data.List using ([])
open import Chu2.ByteString using (pack)
open import Function using (_$_; const)
open import Chu2
postulate
run : ApplicationData → IO Unit
{-# IMPORT Chu2.Handler.SnapServerFFI #-}
{-# COMPILED run Chu2.Handler.SnapServerFFI.run #-}
hello-world-response = response OK [] (pack "Hello Agda!")
hello-world-app : Application
hello-world-app = const $ return hello-world-response
main = run $ chu2 hello-world-app
Note