[Agda] Does Agda2 have fast arrays?

[Conor McBride]

Hi Don

On 3 Oct 2010, at 22:03, Don Stewart wrote:

> conor:
>>
>> 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

GHC Core would be better. After all, there's no point in Agda
doing all that type checking and argument inference, then making
GHC do it again. It's much the better target, provided it
doesn't run away.

Meanwhile, is there any way to get hold of operations like a
putative

   trustFromJust :: Maybe x -> x

which doesn't actually check for Just and Goes Wrong (in Milner's
sense) if fed Nothing?

Cheers

Conor