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