Stream: Beginner Questions

Topic: ✔ Polymorphic HOL vs System F


view this post on Zulip 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.

view this post on Zulip 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 \Rightarrow. 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.

view this post on Zulip 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*)

view this post on Zulip Lukas Stevens (Feb 14 2022 at 11:31):

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"

view this post on Zulip Lukas Stevens (Feb 14 2022 at 11:32):

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.

view this post on Zulip 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"

view this post on Zulip Lukas Stevens (Feb 14 2022 at 11:53):

Yes that is what I was trying to describe.

view this post on Zulip 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.

view this post on Zulip Notification Bot (Feb 14 2022 at 18:38):

waynee95 has marked this topic as resolved.

view this post on Zulip 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: Aug 13 2022 at 05:18 UTC