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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
