Florian Sextl (Apr 15 2022 at 09:17): Florian Sextl (Apr 15 2022 at 09:17):Isabelle/HOL doesn't have type constructor variables (the 'b in '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 Type, TFree and TVar would really fit for this use case.
Manuel Eberl (Apr 15 2022 at 11:38):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.
Lukas Stevens (Apr 15 2022 at 12:07):There is also HOL Omega http://www.trustworthytools.com/id17.html.
Florian Sextl (Apr 15 2022 at 13:50):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.
Notification Bot (Apr 15 2022 at 13:50):Florian Sextl has marked this topic as resolved.
Last updated: Dec 21 2024 at 12:33 UTC