Up to now I used to think that dependent types were only those types such as Pi or Sigma types that require an indexed family of types. However, I was just reminded by a Lean tutorial (if I understood correctly at least) that a dependent type is any type that depends on another type, and lists and products are also dependent types in calculus of constructions. So how does a product work in Isabelle exactly? I guess it still cannot be considered a dependent type from any point of view?

A dependent type is a type that depends on a term, not another type.

Ok thanks I'd guess my question still holds with this correction doesn't it?

You can construct types that depend on other types in isabelle. Those are just type constructors.

Isabelle does not have dependent types. It uses classical logic vs dependent type theory

Eric Bond said:

Isabelle does not have dependent types. It uses classical logic vs dependent type theory

It is based on a simply typed lambda calculus, not classical logic. You can just as well work with non-constructive logics in Isabelle.

The meta-logic Isabelle/Pure is a simply-typed λ-calculus with a rudimentary intuitionistic logic. Using this meta-logic, multiple object logics can be implemented. Several such object logics are part of the Isabelle distribution. The most famous of them is Isabelle/HOL, which is a classical logic. Thus, Kevin is right with respect to Isabelle/Pure, and Eric is right with respect to Isabelle/HOL.

Last updated: Aug 15 2022 at 04:16 UTC