Re: [isabelle] Questions concerning (Haskell) code generation
> 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 ).
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.
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and