[isabelle-dev] Tweak Haskell output for future Haskell compatibility.
bertram.felgenhauer at googlemail.com
Mon May 7 16:02:25 CEST 2012
Dear Isabelle developers,
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.
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 1069 bytes
Desc: not available
More information about the isabelle-dev