[Agda] Does Agda2 have fast arrays?

[Dan Licata]

On Oct03, Don Stewart wrote:
> conor:
> > Hi
> >
> > On 3 Oct 2010, at 08:50, Andreas Abel wrote:
> >
> >> On Oct 3, 2010, at 7:59 AM, Don Stewart wrote:
> >>> nad:
> >>>> On 2010-10-02 18:17, Don Stewart wrote:
> >>>>> Could Agda target one of the high performance array libraries in
> >>>>> Haskell?  E.g. repa or vector?
> >>>>
> >>>> Agda has a Haskell FFI, so that should be easy, assuming that the
> >>>> library APIs don't use too exotic types. However, Agda code is  
> >>>> compiled
> >>>> into Haskell by inserting unsafeCoerce almost everywhere, so I  
> >>>> would not
> >>>> expect good performance, especially if REWRITE pragmas are involved.
> >>>>
> >>>
> >>> What can we do about the coercions? I suspect they make GHC sad.
> >>
> >> The current excessive amount of coercions is not needed.  One could  
> >> write a better compiler using Pierre Letouzey's techniques, who did  
> >> the Coq extraction procedure.  The raw idea is to combine compilation 
> >> with a Hindley-Milner type inference which inserts coercions for you 
> >> when it encounts a type error.
> >
> > Indeed. In any translation from Agda to Haskell, there's going to
> > be some superstructure, like the bit of the iceberg above the water)
> > which typechecks in a Haskelly (which is far more than H-M) way,
> > and some more devilish substructure below the waterline which is
> > too weird for Haskell, hence the use of unsafeCoerce to shut GHC up.
> > The question is "where is the waterline?".
> >
> > The current compiler makes considerable effort to shove almost the
> > whole of the iceberg underwater, despite the fact that it naturally
> > floats. This is understandable as a first attempt, but it's not
> > sustainable.
> >
> > Given Haskell's direction of travel, we can surely take Pierre
> > Letouzey's approach and push it further. Ultimately, compiling
> > via Haskell is not the optimal solution, but it's a good way to
> > get stuff done, bind to other libraries, etc.
> >
> > Meanwhile, I don't know much about GHC, but I do wonder whether,
> > for example, it might be possible to generate faster code for
> > irrefutable patterns which are actually known to be irrefutable.
> > The trouble with compiling via an impure language (I'm talking
> > about you, bottom) with a weaker type system is that the richer
> > information from Agda's types gets thrown away. But perhaps GHC
> > could acquire a "trust me, I'm Agda" flag.
> >
> > So that's two things to think about
> >   (1) can we develop a more (mostly?) typed translation to Haskell?
> >   (2) what fast-but-dangerous code would we like GHC to generate?
> >
> 
> Could we generate GHC Core instead of Haskell (which is fairly direct to
> mark as strict). Also, you have access to System Fc 

Also, as I understand it from the papers, Fc allows you to postulate
arbitrary coercions (which are erased at run-time), which could
potentially be used for the "trust me, I'm Agda" flag.

-Dan