Re: [isabelle] Haskell code generator problem, upper-case type variables

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



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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