[Agda] Does Agda2 have fast arrays?

[Alan Jeffrey]

I hacked around with the Haskell which Agda generates, to make the 
following changes:

a) Only export main,

b) Replace the built-in unsafeCoerce by our own coerce function:

{-# INLINE [1] coerce #-}
coerce :: a -> b
coerce = Unsafe.Coerce.unsafeCoerce

The reason for doing this is to delay the inlining of coercion until 
phase 1.  This allows us to declare some rules for it:

   forall (x :: a) .
     coerce x = x

   forall (f :: a -> b) .
     coerce f = \ x -> (coerce (f (coerce x)))

   forall (x :: (forall a . a)) .
     coerce x = x

   forall (f :: (forall a b . a -> b)) (x :: c) .
     coerce (f (coerce x)) = f x

   forall (x :: Data.Vector.Vector a) .
     coerce x = (Data.Vector.map coerce) x

Run this through ghc, and ta-da:

           68,280 bytes allocated in the heap
            2,968 bytes copied during GC
           36,168 bytes maximum residency (1 sample(s))
           29,368 bytes maximum slop
                1 MB total memory in use (0 MB lost due to fragmentation)

no more memory allocations in the loop.  The rewrites were:

     3 SC:$wfoldlM'_loop0
     4 coerce-beta
     1 coerce-fun
     2 coerce-map
     1 coerce-poly-fun
     4 stream/unstream [Vector]

and the generated Core for the main loop is:

MAlonzo.Main.main_$s$wfoldlM'_loop =
   \ (sc_s1m4 :: GHC.Prim.Int#)
     (sc1_s1m5 :: GHC.Prim.Int#)
     (sc2_s1m6 :: GHC.Prim.Int#) ->
     case GHC.Prim.># sc_s1m4 0 of _ {
       GHC.Bool.False -> sc2_s1m6;
       GHC.Bool.True ->
         MAlonzo.Main.main_$s$wfoldlM'_loop
           (GHC.Prim.-# sc_s1m4 1)
           (GHC.Prim.+# sc1_s1m5 1)
           (GHC.Prim.+# sc2_s1m6 (GHC.Prim.*# 100000 sc1_s1m5))
     }
end Rec }

So it looks like fairly minor modifications to the Agda compiler should 
allow stream fusions to go through.

Hooray!  Got cake!  Eating it!

A.

On 10/04/2010 09:32 PM, Jeffrey, Alan S A (Alan) wrote:
> 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 --------------
A non-text attachment was scrubbed...
Name: Main.hs
Type: text/x-haskell
Size: 2158 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20101005/bb76c2ee/Main-0001.bin