# [isabelle] Haskell code-generation

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] Haskell code-generation
*From*: Christian Sternagel <christian.sternagel at uibk.ac.at>
*Date*: Thu, 31 Mar 2011 09:17:36 +0200
*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.15) Gecko/20110307 Fedora/3.1.9-0.39.b3pre.fc14 Lightning/1.0b2 Thunderbird/3.1.9

Hi all,

`recently I tried to embed some generated code more deeply into the
``Haskell standard library (by using Prelude functions whenever possible).
``The initial problem (which many of you may know) is that whenever in
``Isabelle you are using "nat" the corresponding Haskell function would
``use either Int or Integer... since many Prelude functions are using Int,
``lets just assume that Int should replace "nat" (ignoring the fact that
``nat's may get arbitrarily large but Int's don't).
`

`First HOL/Library/Efficient_Nat.thy seemed exactly to be what I needed,
``but unfortunately it doesn't seem to hold what is claimed in the header:
``"The efficiency of the generated code can be improved
`drastically by implementing natural numbers by target-language
integers. To do this, just include this theory."

`I did just import Efficient_Nat.thy, is there anything else to do
``afterwards (maybe for Haskell Integers are used instead of Int's?).
`

`Does anybody have experience with using Efficient_Nat for Haskell
``code-generation?
`
cheers
chris

`A minor comment: the code-generator setup for Haskell (in HOL.thy)
``declares "&&" and "||" as infixl, whereas in Haskell's Prelude they are
``declared infixr.
`

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