waynee95 (Feb 11 2022 at 18:31): waynee95 (Feb 11 2022 at 18:31):I am trying to get a better understanding of HOL or simpled typed lambda calculus and its variations.
System F seems to be commonly referred to as "polymorphic lambda calculus", I was wondering how exactly it compares to Isabelle/HOL because we also have polymorphism.
Any pointers to papers and other materials to get a better bigger picture, would be appreciated.
Lukas Stevens (Feb 14 2022 at 10:59):The following is my understanding of Isabelle/HOL. System F adds terms depending on types to the simply typed lambda calculus. This is not possible in Isabelle/HOL which uses simply typed lambda calculus. The only type of polymorphism that really exists in Isabelle/HOL is let-polymorphism. In other words, we can universally quantify over type variables in a type but the quantification can only occur at the the top-level; that is, there is no nested quantification beneath type constructors such as the function type constructor . This quantification is exhibited as schematic variables. Isabelle/HOL also allows constant overloading (which is used to realise type classes) but I would call this constant polymorphism and not type polymorphism.
Kevin Kappelmann (Feb 14 2022 at 11:23):Isabelle's schematic polymorphism is weaker than Hindley-Milner let-polymorphism:
term "let id = λx. x in (id (0 :: nat), id ''abc'')" (*type error*)
Due to the definition of let in inner terms, I don't think you can classify this as a proper let:
definition Let :: "'a ⇒ ('a ⇒ 'b) ⇒ 'b"
where "Let s f ≡ f s"
Isabelle/HOL allows you to do this, though: Pow_mono[OF Pow_mono], where the schematic type variables of the theorem are instantiated with different variables for the two occurrences of Pow_mono.
Kevin Kappelmann (Feb 14 2022 at 11:42):That's the thing: there's no special support for polymorphism for local let definitions.
Some describe Isabelle's schematic polymorphism as "Hindley-Milner let-polymorphism without a local let"
Lukas Stevens (Feb 14 2022 at 11:53):Yes that is what I was trying to describe.
Lukas Stevens (Feb 14 2022 at 11:54):Kevin Kappelmann said:
That's the thing: there's no special support for polymorphism for local let definitions.
Some describe Isabelle's schematic polymorphism as "Hindley-Milner let-polymorphism without a local let"
It should be possible to implement this, though.
Notification Bot (Feb 14 2022 at 18:38):waynee95 has marked this topic as resolved.
Manuel Eberl (Feb 18 2022 at 15:53):Lukas Stevens said:
Kevin Kappelmann said:
That's the thing: there's no special support for polymorphism for local let definitions.
Some describe Isabelle's schematic polymorphism as "Hindley-Milner let-polymorphism without a local let"It should be possible to implement this, though.
Logically perhaps, but in the system we have I don't think it would be possible. This would require you to make a new toplevel definition for every ‘let’ you encounter during type checking. And Isabelle does not allow you to add new constants during type checking. (which would be pretty crazy)
Last updated: Apr 20 2024 at 12:26 UTC