Re: [isabelle] Uses of type quantification



John Matthews wrote:
Hello,

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 mechanism.

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.

Jeremy





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