[Agda] Does Agda2 have fast arrays?

[Andreas Abel]

My response has been left out of the loop (should not have switched  
subject).

On Oct 3, 2010, at 11:36 PM, Don Stewart wrote:

> 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};

I think what Conor meant is that the the y is projected out directly,  
without a case statement verifying that the tag "Just" is present.

Is this compiled like Conor would expect?

> 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.

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/