[Agda] Does Agda2 have fast arrays?

[Conor McBride]

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?

Interesting times...

Conor

PS Beware Haskell groupthink. We must not let an improving
Agda-Haskell connection (technically and socially) fool us into
adopting Haskell-like approaches to design issues by default.
We have a golden opportunity to think again. Let's not blow it.
When I hear people say, effectively, "I want to program with
dependent types, but I don't want to learn anything new." I feel
like I should scream, and sometimes I actually do.