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 :)
This archive was generated by a fusion of
Pipermail (Mailman edition) and