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.
Last updated: Jul 15 2022 at 23:21 UTC