Stream: Beginner Questions

Topic: Product in simple type theory


view this post on Zulip Nicolò Cavalleri (Sep 09 2021 at 16:31):

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?

view this post on Zulip Kevin Kappelmann (Sep 09 2021 at 16:33):

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

view this post on Zulip Nicolò Cavalleri (Sep 09 2021 at 16:36):

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

view this post on Zulip Kevin Kappelmann (Sep 09 2021 at 16:42):

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

view this post on Zulip Eric Bond (Sep 13 2021 at 14:38):

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

view this post on Zulip Kevin Kappelmann (Sep 14 2021 at 17:16):

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.

view this post on Zulip Wolfgang Jeltsch (Sep 14 2021 at 18:37):

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