Nicolò Cavalleri (Sep 09 2021 at 16:31): 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?
Kevin Kappelmann (Sep 09 2021 at 16:33):A dependent type is a type that depends on a term, not another type.
Nicolò Cavalleri (Sep 09 2021 at 16:36):Ok thanks I'd guess my question still holds with this correction doesn't it?
Kevin Kappelmann (Sep 09 2021 at 16:42):You can construct types that depend on other types in isabelle. Those are just type constructors.
Eric Bond (Sep 13 2021 at 14:38):Isabelle does not have dependent types. It uses classical logic vs dependent type theory
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.
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: Apr 19 2024 at 16:20 UTC