[Agda] Does Agda2 have fast arrays?

[Alan Jeffrey]

On 10/04/2010 05:10 PM, Don Stewart wrote:
> Well, you usually don't write in Streams directly, they're used at a concrete type.
> Vector is a good example of a fusible library.

Yes, I started with Data.Vector, got confused as to why the 
optimizations weren't happening, and decided to try the bare metal to 
see if that helped.

> Also, concatMap doesn't fuse.  (It is the hardest thing to fuse (Stream (Stream ..)))
>
>      -- NOTE: We can't fuse concatMap anyway so don't pretend we do.
>      -- concatMap f = unstream . Stream.concatMap (stream . f) . stream

Ah, I only read the first half of your paper, where this example is the 
poster child, and didn't read the end of section 7, which talks about 
the problems with concatMap.

> So, let's start with something simpler.
>
>      import qualified Data.Vector as V
>
>      f :: Int ->  Int
>      f n = V.sum $ V.map (\m ->  n * m) (V.enumFromN 1 n)
>
>      main = putStr (show (f 10000))

OK, I ported this to Agda (attached, though it's not very exciting) and 
indeed it fails to optimize away the intermediate vectors.  Rather than:

>      203 PreInlineUnconditionally
>      94 PostInlineUnconditionally
>      95 UnfoldingDone
>      5 RuleFired
>          3 SC:$wfoldlM'_loop0
>          2 stream/unstream [Vector]
>      13 LetFloatFromLet
>      1 EtaReduction
>      313 BetaReduction
>      3 CaseOfCase
>      65 KnownBranch
>      1 CaseIdentity
>      1 FillInCaseDefault
>      21 SimplifierDone

it gets:

939 PreInlineUnconditionally
542 PostInlineUnconditionally
579 UnfoldingDone
42 RuleFired
     2 0# +# x#
     5 SC:$wa0
     6 SC:$wfoldlM'_loop0
     1 coerce=id
     13 unpack
     13 unpack-list
     2 x# +# 0#
63 LetFloatFromLet
1 EtaReduction
1823 BetaReduction
11 CaseOfCase
348 KnownBranch
4 CaseIdentity
8 FillInCaseDefault
19 SimplifierDone

Note: no stream/unstream rewrites.  I tried adding rule:

{-# RULES "coerce=id" forall (x :: a) . unsafeCoerce x = x #-}

but (as you can see) it only fired once, sigh.  It maybe that 
unsafeCoerce is being inlined before optimized, unfortunately trying to 
optimize the primitive:

{-# RULES "coerce#=id" forall (x :: a) . unsafeCoerce# x = x #-}

is a syntax error!  (Apparently rules don't like identifiers with #s in 
their names.)  Somewhat annoying, since (AFAICT) most of the occurrences 
of unsafeCoerce are actually statically of type a->a, so should be 
removeable by the rule coerce=id.

> -- Don

A.
-------------- next part --------------
open import Data.String using ( String )
open import Foreign.Haskell using ( fromString )
open import IO.Primitive using ( putStr )

module Main where

postulate 
  Int : Set
  one : Int
  oneE5 : Int
  _*_ : Int → Int → Int
  show : Int → String

{-# COMPILED_TYPE Int Int #-}
{-# COMPILED one 1 #-}
{-# COMPILED oneE5 100000 #-}
{-# COMPILED _*_ (*) #-}
{-# COMPILED show show #-}

postulate
  Vector : Set → Set
  map : {A B : Set} → (A → B) → (Vector A) → (Vector B)
  sum : (Vector Int) → Int
  enumFromN : Int → Int → (Vector Int)

{-# IMPORT Data.Vector #-}
{-# COMPILED_TYPE Vector Data.Vector.Vector #-}
{-# COMPILED map (\ _ _ -> Data.Vector.map) #-}
{-# COMPILED sum Data.Vector.sum #-}
{-# COMPILED enumFromN Data.Vector.enumFromN #-}

{-# IMPORT Rules #-}

f : Int → Int
f n = sum (map (λ m → n * m) (enumFromN one n))

main = putStr (fromString (show (f oneE5)))
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Rules.hs
Type: text/x-haskell
Size: 121 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20101004/b626b7e2/Rules.bin