*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Haskell code generator problem, upper-case type variables*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Mon, 05 Oct 2009 08:43:49 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4AC78207.1020206@uni-muenster.de>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <4AC78207.1020206@uni-muenster.de>*User-agent*: Thunderbird 2.0.0.23 (X11/20090817)

Hi Peter, > I have a problem with the Haskell code generator. It generates > upper-case type variables, that are not accepted by ghci 6.4.10. > Is this problem known? Is there any workaround (ghci configuration?) > other than working through all theories and only using lowe-case > type-variables, which I definitely do not want? I must admit that this problem slipped into Isabelle 2009 accidentally. For Haskell there is no workaround since lower/upper case distinction is essential to distinguish between type constructors and type variables. One workaround could be to redeclare each code theorem with lower case type variables, in our toy example: definition test_fun :: "('a \<Rightarrow> 'S) \<Rightarrow> 'a \<Rightarrow> ('S\<times>'S)" where "test_fun f x = (f x, f x)" declare test_fun_def [where ?'S = 's, standard, code] but this is not convincing either. If you really bother substituting all type variables e.g. by means of a perl one-liner, let me know, and I will provide you with a patch for the Isabelle 2009 sources. Hope this helps Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**[isabelle] Haskell code generator problem, upper-case type variables***From:*Peter Lammich

- Previous by Date: Re: [isabelle] Formalizing Turing machine
- Next by Date: [isabelle] Syntax translation for types
- Previous by Thread: [isabelle] Haskell code generator problem, upper-case type variables
- Next by Thread: [isabelle] Syntax translation for types
- Cl-isabelle-users October 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list