Compilation [Re: [Agda] Does Agda2 have fast arrays?]

[Andreas Abel]

Hi Conor,

good thoughts (and a good metaphor!).

Compiling to (GHC-)Haskell basically gives you a choice:

1. Compile to Haskell source

Advantage: People know source Haskell.  (However, the current  
translation from Agda does not produce much legible code anyway).

Disadvantage: Haskell source does not have a construct for type  
application, and not all instantiations can be guessed by the Haskell  
type checker correctly.  However, we already have the type arguments  
in Agda, why throw them away and give GHC the task to reconstruct them.

2. Compile to Haskell core

Advantage: this is closer to Agda internal syntax.  Has type  
abstraction and application.

Disadvantage: I don't know how well it is supported and whether .hcr  
modules can be properly imported.

   http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/ext-core.html

says:

   Currently (as of version 6.8.2), GHC does not have the ability to  
read in External Core files as source. If you would like GHC to have  
this ability, please make your wishes known to the GHC Team.

For the near future, it will be Haskell source, then, unless we find a  
friend who fully integrates External Core files into GHC.

There are other choices, like whether Agda inductive families should  
be compiled to GADTs.  In some sense, we don't want to compile into a  
fancy type system, we could as well compile to untyped lambda- 
calculus, as long as the backend still does the optimizations.

Cheers,
Andreas


On Oct 3, 2010, at 12:18 PM, Conor McBride wrote:
> 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.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/