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



Rafal Kolanski wrote:
Dear Isabelle Gurus,

...

What I want to do is to define a type class which fixes some parameter over multiple types. Intuitively, to go from "'a set" and "'a list" to "'a container", which means something like "'a (set OR list)", so I could define:



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)

Jeremy







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