Re: [isabelle] Questions concerning (Haskell) code generation



Am 12.12.2011 13:03, schrieb Florian Haftmann:
> Hi René,
> 
>> 1.) It is in someway possible to make the generated code have an
>> explicit export list? So something like
>>
>> export_code bla foo [export] in Haskell module_name Code file -
>>
>> that results in the following module definition
>>
>> module Code (bla, foo) where ...?
>>
>> The reason is, that w/o an explicit export list the compiler assumes
>> that all functions are exported and therefore does not inline them or
>> uses other code optimizations (see [1]).
> 
> this is an interesting observation.  Up until now, I did not pay much
> attention to export lists, in order to keep things as simple as
> possible.  So far I did not consider inlining issues.  There are
> important enough to reconsider hiding and exporting anew.  Anyway,
> analysis and implementation will take considerable time.

This sounds like you plan on adding some sort of automated generation of
export lists. Would be as hard to implement some additional syntax that
gives the user the choice of specifying the export list that is going to
be generated (I don't know though whether this concept is useful for the
other languages...)? Just to avoid having to edit auto-generated files.


>> 2.) I noted that when using "Efficient_Nat", I got two new types for
>> natural numbers in code: Natural and Nat. The code of both looks nearly
>> identical (see attached files) and also only one of them (Nat) is used
>> throughout the rest of the code. Is there a deeper reason behind having
>> them both?
> 
> Consider type classes: there is only one instantiation of a type per
> class;  this prohibits to map two different types in the logic onto the
> same type in Haskell.  This affects all languages with implicit
> dictionaries, i.e. also Scala, but not SML/Ocaml.

Thanks for the explanation.

- René





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.