# [isabelle] Haskabelle configuration

Dear Haskabelle developers,

`I am trying to import some Haskell code using Haskabelle for Isabelle2011-1. So
``far, I ran into the following two problems:
`
1. Bound variable names clash with previous constant names.
For example, in the following Haskell program
f = \x -> x
g = f
h f = (f, g)
f is bound in h's definition, but also defined previously.
Haskabelle generates the following definitions in Isabelle:
definition f where "f = (% x . x)"
definition g where "g = f"
fun h where "h f = (f, g)"

`Obviously, this is not what I want, because h's definition now "pattern-matches"
``on the constant f, but it should actually be as follows:
`
fun h where "!!f. h f = (f, g)"

`The same problem also occurs with predefined constants from the Isabelle
``library. I suggest that Haskabelle explicitly adds the universal quantification
``to all bound variables that occur on the left-hand equation of a function
``definition such that it need not know which names are used.
`

`Is there some other way than manually renaming all such variables in the Haskell
``code? This is something I actually want to avoid.
`
2. do notation

`Apparently, Haskabelle has some undocumented support for do notation and monads.
``At least, this is what I gather from the files in ex/ and the error message for
``the following program:
`
f = do {
x <- [1,2];
y <- [x + 1];
[y]
}
haskabelle_bin: Do syntax is used without sufficient type information!

`What type information do I have to add (and where) such that such examples
``compile? Actually, I would have expected that no type information were
``necessary, because Isabelle's parser setup for do notation in
``Library/Monad_Syntax should resolve the operations correctly.
`Can I configure Haskabelle to use that setup?
Thanks for any help,
Andreas
--
Karlsruher Institut für Technologie
IPD Snelting
Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de

`KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum
``in der Helmholtz-Gemeinschaft
`

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