Agda as a Programming Language: Using Haskell for basically everything

Agda would not be useful if it had to reinvent all of its wheels. Luckily it is faily easy to use Haskell from Agda.

     wordcount.agda 

  1  module wordcount where
  2  
  3  import Foreign.Haskell as Hask
  4  open import IO.Primitive renaming (putStrLn to putStrLnCo)
  5  open import Data.List
  6  open import Data.String
  7  open import Function using (_∘_)
  8  
  9  -- Data.Nat is unary. This is terribly inefficient. Ideally
 10  -- we would use Haskell numbers, but that is not convenient.
 11  open import Data.Nat
 12  
 13  -- Data.Nat.Show was written before Agda had typeclass support.
 14  open import Data.Nat.Show renaming (show to showNat)
 15  open import Data.Char
 16  
 17  putStrLn = putStrLnCo ∘ toCostring
 18  
 19  infixl 1 _>>_
 20  postulate
 21      _>>_  : ∀ {a b} {A : Set a} {B : Set b} → IO A → (IO B) → IO B
 22  {-# COMPILED _>>_  (\_ _ _ _ -> (>>)) #-}
 23  
 24  module CmdlineArgs where
 25      {-# IMPORT System #-}
 26      postulate sysArgs : IO (List String)
 27      {-# COMPILED sysArgs (System.getArgs) #-}
 28  
 29  module FileIO where
 30      {-# IMPORT System.IO #-}
 31      postulate Handle : Set
 32      {-# COMPILED_TYPE Handle System.IO.Handle #-}
 33      postulate hGetLine : Handle -> IO String
 34      {-# COMPILED hGetLine (System.IO.hGetLine) #-}
 35      postulate hGetContents : Handle -> IO String
 36      {-# COMPILED hGetContents (System.IO.hGetContents) #-}
 37      postulate IOMode : Set
 38      {-# COMPILED_TYPE IOMode System.IO.IOMode #-}
 39      postulate ReadMode : IOMode
 40      {-# COMPILED ReadMode (System.IO.ReadMode) #-}
 41      -- This won't work if it's not universe-polymorphic. I Don't know why.
 42      postulate withFile : ∀ {u} {A : Set u} -> String -> IOMode -> (Handle -> IO A) -> IO A
 43      {-# COMPILED withFile (\_ _ -> System.IO.withFile) #-}
 44  
 45  open CmdlineArgs
 46  open FileIO
 47  
 48  wordsInString : String -> ℕ
 49  wordsInString s = ws1 (toList s) where
 50      mutual
 51          ws1 : List Char -> ℕ
 52          ws1 [] = 0
 53          ws1 (' ' ∷ rest) = ws1 rest
 54          ws1 (c ∷ cs) = suc (ws2 cs)
 55  
 56          ws2 : List Char -> ℕ
 57          ws2 [] = 0
 58          ws2 (' ' ∷ rest) = ws1 rest
 59          ws2 (c ∷ cs) = ws2 cs
 60  
 61  -- Agda does not have case expressions, so we use a local
 62  -- function to pattern match.
 63  main : IO Hask.Unit
 64  main = sysArgs >>= doArgs where
 65      -- Agda's type inference is not as good as Haskell's;
 66      -- We have to specify some amount of signature.
 67      doArgs : _ -> _
 68      doArgs (path ∷ []) =
 69          withFile path ReadMode \hl ->
 70              hGetContents hl >>= \text ->
 71              let count = wordsInString text in
 72              putStrLn (showNat count)
 73      doArgs _ =
 74          putStrLn "Usage: wordcount <filename>"

• IMPORT, COMPILED and COMPILED_TYPE do what they seem like.
• There is also COMPILED_DATA, but his program didn't use it. There are some examples in the standard library.