Re: [isabelle] Uses of type quantification
John Matthews wrote:
Brian Huffman, Peter White, and I are interested in having a limited
form of type quantification added to Isabelle/HOLCF. It turns out that
many of Haskell's constructor classes (most notably functors and monads)
are associated with axioms that require quantifying over type variables.
An alternative way of handling this situation would be to actually have
constructor classes, as a generalisation of the present type class
I don't know whether this would be feasible, but I recall reading
something about the development of Haskell which seemed to suggest
that constructor classes, as a generalisation of type classes, use
rather similar mechanisms.
This archive was generated by a fusion of
Pipermail (Mailman edition) and