[Agda] Does Agda2 have fast arrays?

[Alan Jeffrey]

On 10/03/2010 12:59 AM, Don Stewart wrote:
> What can we do about the coercions? I suspect they make GHC sad.

Sorry, I'm being dense here -- what's the runtime penalty for 
unsafeCoerce?  I'd expect that most compilers implement it as a no-op.

There may be cases where ghc's optimizer can't do as good a job because 
of unsafeCoerce, due to lack of type information, but I doubt that would 
have much of an impact in practice.

As a dumb benchmark, I merge-sorted 20K of data, first in Agda:

1.23user 0.48system 0:01.72elapsed 99%CPU (0avgtext+0avgdata 
1282352maxresident)k
0inputs+48outputs (0major+80211minor)pagefaults 0swaps

then in Haskell:

1.22user 0.64system 0:01.85elapsed 100%CPU (0avgtext+0avgdata 
1282368maxresident)k
0inputs+48outputs (0major+80212minor)pagefaults 0swaps

This is a deliberately (honest!) not-very-clever sorting algorithm which 
generates lots of cons cells.  I ran it with 2G heap to minimize the 
impact of the GC (about 13% GC time).

Of course, you can argue that this isn't a very good benchmark, as it is 
more memory-intensive than cpu-intensive.  But it's looking to me like 
the Agda overhead is pretty insignificant.  There may be other reasons 
for wanting less coercion though, e.g. less retypechecking, targeting 
languages (e.g. Java) which don't have a no-op coercion...

A.
-------------- next part --------------
{-# OPTIONS --no-termination-check #-}

open import Coinduction using ( ♭ ; ♯_ )
open import Data.Char using ( Char )
open import Data.Bool using ( Bool ; true ; false )
open import Data.Product using ( _×_ ; _,_ )
open import IO.Primitive using ( getContents ; putStr ; _>>=_ )
open import Foreign.Haskell using ( Colist ; []; _∷_ )

module Main where

postulate _<_ : Char → Char → Bool
{-# COMPILED _<_ (<) #-}

Costring = Colist Char

merge : Costring → Costring → Costring
merge xs     []             = xs
merge []     ys             = ys
merge (x ∷ xs) (y ∷ ys) with x < y
... | true  = x ∷ ♯ merge (♭ xs) (y ∷ ys)
... | false = y ∷ ♯ merge (x ∷ xs) (♭ ys)

split : Char → Costring → Costring → Costring → (Costring × Costring)
split x xs ys []             = (xs , ys)
split x xs ys (z ∷ zs) with x < z 
... | true  = split x xs (z ∷ ♯ ys) (♭ zs)
... | false = split x (z ∷ ♯ xs) ys (♭ zs)
  
sort : Costring → Costring
sort [] = []
sort (x ∷ xs) with split x [] [] (♭ xs)
... | (ys , zs) = merge (sort ys) (x ∷ ♯ sort zs)

main = getContents >>= λ x → (putStr (sort x))

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Main.hs
Type: text/x-haskell
Size: 588 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20101004/37e28275/Main.bin