[isabelle-dev] Tweak Haskell output for future Haskell compatibility.

[Florian Haftmann]

Hi Bertram,

> the Haskell code generator of Isabelle currently emits contexts for
> data and newtype generates, e.g. (from CeTA):
> 
>   newtype (Linorder a) => Rbt a b = Rbt (Rbta a b);
> 
> The sole effect of such contexts is that the programmer must provide
> a (Linorder a) context wherever Rbt a b is used, which is fairly uselss.
> In the next version of the Haskell language definition (whenever that
> will be), this feature will be removed.
> 
>   http://www.haskell.org/pipermail/haskell-prime/2011-January/003335.html
>   http://hackage.haskell.org/trac/haskell-prime/wiki/NoDatatypeContexts
> 
> Ghc currently requires a flag (-XDatatypeContexts) to compile code
> using datatype contexts. In the latest release (7.4.1), this option
> emits a warning:
> 
>     Warning: -XDatatypeContexts is deprecated: It was widely considered a
>     misfeature, and has been removed from the Haskell language.
> 
> I propose, therefore, to omit these contexts in code generated by
> Isabelle. This can safely wait until after the release, of course.
> (patch attached)

thanks for pointing that out.  Indeed, the incorporation of contexts (in
Haskell speak, in Isabelle we denote this rather as sort constraints)
for datatype constructors into the code generator is a relict of the
early days of the code generator when I approached this story
(necessarily) in a rather naive way.  Since there was never a urgent
pain to remove this »feature«  it remained as it is.  In the next months
(i.e. before the release *after* Isabelle-2012) I will take care of this
clean it up.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120513/3252c068/attachment.sig>