[Agda] Call by name vs call by need

[Swierstra, W.S. (Wouter)]

Dear all,

I've implemented a generic memo-structure for memoising recursive 
computations in Agda. The idea -- originally due to Ralf Hinze [1], 
packaged in Haskell by Spencer Janssen and Conal Elliott [2,3] -- relies 
on lazy evaluation to share the memo structure across different 
recursive calls.

Unfortunately, I don't seem to be able to reproduce the same kind of 
speedup in Agda as I can in Haskell -- and I can't figure out why. My 
understanding is that the Agda Abstract Machine uses a call by need 
reduction strategy, that can optionally be disabled. But it seems like 
the structure isn't being shared properly once it has been constructed. 
Is there any way to verify/debug this? Or any other information about 
how (sharing in) the Agda Abstract Machine works? I realise that 
compiling the code to Haskell would improve performance, but I'm 
particularly interested speeding up code evaluated at compile time -- so 
that wouldn't be much help.

Thanks in advance for any pointers,

   Wouter

[1] - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.4069
[2] - https://hackage.haskell.org/package/MemoTrie
[3] - 
http://conal.net/blog/posts/elegant-memoization-with-functional-memo-tries