Isabelle/HOL doesn't have type constructor variables (the
'a 'b), which are e.g. necessary for a monad type class. I've found several occurrences of the claim that HOL can't have such variables but I can't really find any evidence on why this holds. Could anyone here give me a hint to why we can't simply extend HOL with higher kinded type variables?
The only technical limitation for Isabelle/HOL that I can think of would be that there is no corresponding ML representation in Pure. None of
TVar would really fit for this use case.
I don't know much about such things but my guess would be that it is definitely possible to do implement an Isabelle/HOL object logic that does such a thing, but you would have to build your own type system to accommodate it. In Isabelle/HOL, Isabelle/HOL types are just Isabelle/Pure types, which is nice and makes things much easier in implementation.
E.g. Josh Chen's implementation built a dependently-typed system on top of Isabelle/Pure, which is possible, but requires a lot of extra plumbing.
Building something like this on top of Isabelle/HOL is probably possible, but it would definitely not be as nice to use as the current HOL.
There is also HOL Omega http://www.trustworthytools.com/id17.html.
So it really is more of technical issue (plus the overhead of not using the Pure types). Thank you for the insights and the interesting pointers.
Florian Sextl has marked this topic as resolved.
Last updated: Aug 15 2022 at 04:16 UTC