Re: [isabelle] A parametrised type class for two or more parametrised types?




Jeremy Dawson wrote:
this looks like the issue of having (type) constructor classes as well as just type classes, as was introduced into Haskell some time ago.

Sadly Isabelle (and ML, unlike Haskell) has a language of _types_ which is not higher order (ie, ('a, 'b) tycon, where tycon is not variable, in contrast to Haskell's tycon a b, where a and b can be types (of kind TYPE), or type constructors (of kind TYPE -> TYPE), etc)

Thank you, Jeremy. I had a feeling that I'm at the edge of the type system.
I'm currently getting around the issue by performing the instantiation in a separate theory which can be swapped to a different one. This sort of "modularity" though relies heavily on documentation in plain English :)

Sincerely,

Rafal Kolanski.






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