[Agda] Does Agda2 have fast arrays?

[Don Stewart]

ajeffrey:
> 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.

It's a no-op, that generates a constraint type:

    ActualType ~ CoerceType

And doing so creates a bit of an optimization boundary.
 
> 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).

But we'd like to use arrays (e.g.
http://hackage.haskell.org/package/vector) not lists, right?
 
    > 
    > split :: Char -> [Char] -> [Char] -> [Char] -> ([Char],[Char])
    > split x xs ys []             = (xs,ys)
    > split x xs ys (z:zs) | x < z = split x xs (z:ys) zs
    > split x xs ys (z:zs)         = split x (z:xs) ys zs
    >   
    > sort :: [Char] -> [Char]
    > sort [] = []
    > sort (x:xs) = merge (sort ys) (x : sort zs) where (ys,zs) = split x [] [] xs
    > 
    > main = getContents >>= putStr . sort

I'm mostly interested in embeddings that take advantage of fast
"backends" from Hackage.

-- Don