[isabelle-dev] [isabelle] New representation of naturals in Code_Target_Numeral decreases generated code performance

[Andreas Lochbihler]

Hi Florian,

newtype in Haskell is not always for free, see for example Joachim's blog post: 
http://www.joachim-breitner.de/blog/archives/610-Adding-safe-coercions-to-Haskell.html

Andreas

On 19/09/13 12:58, Florian Haftmann wrote:
> Hi Peter,
>
>> When using Code_Target_Numeral instead of the old Efficient_Nat, the
>> code generator wraps some funny dummy-datatype (nat = Nat of int) around
>> my natural numbers.
>>
>> What was the reason behind this change, and is there a way to produce
>> code working with plain IntInf?
>
> There have been two reasons:
> * Proper datatype abstractions: negative integers are not natural
> numbers; no explicit check necessary for subtraction of natural numbers.
> * When Haskell type classes or Scala implicits are involved, it is
> necessary that the mapping of HOL types to target language types is
> injective.  The coping with this was nightmare in the previous situation
> and is now straight-forward.
>
> As a preface, I have checked these change previously against
> Flyspeck_Tame and did not notice any performance difference.
>
>>> For one of my benchmarks (heavy use of arrays in
>>> Imperative-HOL) this results in doubling the runtime under PolyML. Under
>>> mlton, its only around 15% slower.
>
> Quoting Andreas:
>> In many cases, such type copies do not affect performance, because the compiler can get rid of such type copies after type checking. However, when they are nested into some other polymorphic type, this is not always possible. Maybe, arrays fall into that class.
>
> I am not sure about that.  If this is the case then I wonder how the
> contract in Haskell that »newtype« declarations are always compiled away
> is accomplished in Haskell.  Or maybe there is some ML subtlety creeping
> in here?  Maybe we should contact David Matthews on that.
>
> Another possibility is that the code setup for Imperative-HOL contains a
> performance flaw.  Have you a change to figure out which functions are
> the top-wasters in your benchmark?  Then we could inspect these.
>
> Hope this helps,
> 	Florian
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>