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.

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.

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`

.

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"

Yes that is what I was trying to describe.

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.

waynee95 has marked this topic as resolved.

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: Sep 25 2022 at 22:23 UTC