[Agda] Does Agda2 have fast arrays?

[Don Stewart]

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

The best way would be to generate the core for this (e.g. after the
"FillInCaseDefault" pass.

    %module main:A
      main:A.trustFromJust :: %forall t . (base:DataziMaybe.Maybe t) -> t =
        \ @ t (x::(base:DataziMaybe.Maybe t)) ->
            %case t x %of
               base:DataziMaybe.Just (y::t) -> y};

But GHC doesn't accept .hcr input at the moment. 

Another way might be to use unpackClosure# (e.g. like the vacuum library does , to render the heap).

Yet another would be to write a  -fdisable-fill-in-case-default that turns off that bit of code.

-- Don