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

[Florian Haftmann]

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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130919/56557ad2/attachment.asc>