[Agda] Does Agda2 have fast arrays?

[Don Stewart]

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