6 ms·

>It is based on dependent products which you need to understand sooner-or-later (sooner, really), Type-theoretic universal quantification _is_ the dependent pr

>It is based on dependent products which you need to understand sooner-or-later (sooner, really), Type-theoretic universal quantification _is_ the dependent product (/dependent function, a term I prefer). I assume you're talking about the Cartesian representation, but that's just one way to visualize it, the definition is not dependent on it. If you understand predicate logical quantification it's not necessary at all, since the introduction/elimination rules for type theoretic quantification are the same as for normal predicate logic quantifiers. >are rather more intricate than FOL Maybe in application and theoretical implications, but to grasp the concept you have just have to understand that it's relaxing the restriction on "what you can quantify over", which really isn't a huge jump I'd say. > Ah, but that's the thing. It's not a function and it can't be (for the same reason you don't have an identity function in set theory). Why would it not be a function? With set theory you have the issue that you can't take a set as an argument and have the codomain and it's elements be dependent on it, but that's exactly what dependent function types allow you to do. The universe U is a sort and A is a valid sort too, so forall A:U. forall a : A. A is a perfectly valid function signature and the term would just be (lambda A : U. lambda a : A. a). That doesn't strike me as any more complicated than your second TLA+ example. Sure, you have to deal with universe polymorphism, but I'd say that's compensated by the increased complexity from having to use syntactic operator. Lean's syntax to specify the universe U is admittedly pretty ugly, but the actual meta-theory isn't that complex I'd say.

pron 6y ago
> Maybe in application and theoretical implications, but to grasp the concept you have just have to understand that it's relaxing the restriction on "what you can quantify over", which really isn't a huge jump I'd say. It's not that. It's hard for me to try and quantify some essential complexity of a type theory and a set theory, but programmers don't usually learn type theory in high-school or college, but FOL comes "for free" (not to mention the unnecessary complication of constructive mathematics with special handling of noncomputable functions for specifying digital systems) and engineers don't even need to learn the inference rules, because they will rarely bother writing proofs; just pressing the button on the model checker has a much better cost/benefit, plus it allows learning just semantics first, even you do want to learn deduction later. With TLA+ there isn't much to grasp or learn; you know most of the basics. It could just be a situational thing. > Why would it not be a function? What is the type of its first argument? IIRC, in Lean, it is only a function when a specific universe is given (implicitly).
- ImprobableTruth 6y ago
  I'd agree that people are generally going to be less familiar with type theory (though I think it's not uncommon to touch on the simply typed lambda calculus in undergrad courses), but I really think anybody who has all those prerequisites could also learn enough type theory to write specifications in a couple hours because you don't actually need a deep understanding of type theory to use it (though maybe you meant that you immediately started writing specifications of large, real-world systems in TLA+, but I'd presume you'd then be the outlier on that). In my experience people pick up Isabelle (/HOL) really quickly and writing specifications in a type theory based proof assistant isn't a huge jump from that. Now, writing actual proofs is a completely different matter, but I didn't disagree with you on how economical/ergonomic the over all approach actually is, just the basic complexity of the theory/specifications ;) >What is the type of its first argument? Some universe U, which is an implicit argument. You could alternatively write your Lean example as def id {u} {α : Sort u} (a : α) : α := a Not being able to specify the type of u in Lean might seem kinda cheaty, but I'd say that's similar to how one declares generic type parameters in e.g. Java. You wouldn't say that those languages' generic functions aren't actually functions, would you? Similar to how one could make those generics explicit, it is actually possible to define a special type of all universes (not including itself). Agda does this by having a special primitive type of universe levels. As an example id : forall {u : Level} -> forall {A : Set u} -> A is the signature of the universe polymorphic identity function. The Level type doesn't you any issues because it is essentially a 'top' type that doesn't have a type itself.
  - pron 6y ago
    > but I really think anybody who has all those prerequisites could also learn enough type theory to write specifications in a couple hours because you don't actually need a deep understanding of type theory to use it That has not been my experience. Typed formalisms have further complications with "partial" functions -- either they're actually partial, which is a rather complex concept, or you need refinement types to define them, as well as with constructive mathematics, which isn't necessary for specification. Plus, what are you going to do with your specifications after a few hours if you can't write proofs after few hours (or a few days)? And because of that the tutorials don't and won't just teach specification first and proof later -- as the TLA+ tutorials do -- so even if this were hypothetically true, you have nowhere to learn things like that. Lean has very good tutorials, and you can compare how far they get how quickly with the TLA+ tutorials. I don't know if it's even possible to teach such formalisms the same way as TLA+, but even if it were possible, I haven't seen such tutorials. Those languages are so infused with their formalism's proof theory that it's hard to separate the two [1]. For example, most typed formalisms define integer division by zero to equal zero. Suppose they didn't, and they wanted to teach how to define division "properly". How much would a student need to know in order to define and use the div function? OTOH, TLA+ handles partiality in what I think is a simpler way, with a careful definition of Hilbert's epsilon operator (see https://pron.github.io/posts/tlaplus_part2#the-choose-operator-and-the-meaning-of-undefined https://pron.github.io/posts/tlaplus_part2#the-choose-operat...) Finally, most specifications people in industry are interested in are not of sequential algorithms but concurrent ones, which you also can't do after a few hours (or a few days). > In my experience people pick up Isabelle (/HOL) really quickly Depends what you mean by "really quickly." Isabelle has some accidental complications such as the nested languages. But I think something like Why3 can be picked up quickly, although it doesn't handle concurrency easily. > Not being able to specify the type of u in Lean might seem kinda cheaty, but I'd say that's similar to how one declares generic type parameters in e.g. Java. You wouldn't say that those languages' generic functions aren't actually functions, would you? The type system in Java or Haskell cannot be used as a sound mathematical foundation, so whatever I call those things it would mean something quite different from maths functions. I call them subroutines, but those that call them functions know (I hope) that they're overloading the term. In any event, students that do learn simply typed lambda calculus learn it in the context of programming languages whose type systems are inconsistent and they certainly don't learn how to do maths with them. Anyway, `id` is not a function in Lean because the universe argument doesn't have a type. But I wonder, in Agda, is `id id` some object even when a specific universe cannot be inferred? If so, how does Agda avoid Russel's paradox? [1]: Which I think is a big problem. The clean separation of model and proof is an important property of a formal logic designed for ease of learning, expression and comprehension, and we must not forget that ease of learning, expression, and comprehension -- so that practitioners rather than logicians will be able to make everyday use of it -- has been a central goal of formal logic since at least Frege, if not Boole or even Leibniz, equal in importance to, if not superseding, that of mechanical proof. I might be getting carried away, but I think that TLA+ is a pretty special accomplishment in the history of formal logic in that it is perhaps the first truly rich formal logic that is commonly used by non-specialist practitioners in their day-to-day work.

pron 6y ago

> Maybe in application and theoretical implications, but to grasp the concept you have just have to understand that it's relaxing the restriction on "what you can quantify over", which really isn't a huge jump I'd say. It's not that. It's hard for me to try and quantify some essential complexity of a type theory and a set theory, but programmers don't usually learn type theory in high-school or college, but FOL comes "for free" (not to mention the unnecessary complication of constructive mathematics with special handling of noncomputable functions for specifying digital systems) and engineers don't even need to learn the inference rules, because they will rarely bother writing proofs; just pressing the button on the model checker has a much better cost/benefit, plus it allows learning just semantics first, even you do want to learn deduction later. With TLA+ there isn't much to grasp or learn; you know most of the basics. It could just be a situational thing. > Why would it not be a function? What is the type of its first argument? IIRC, in Lean, it is only a function when a specific universe is given (implicitly).

ImprobableTruth 6y ago
I'd agree that people are generally going to be less familiar with type theory (though I think it's not uncommon to touch on the simply typed lambda calculus in undergrad courses), but I really think anybody who has all those prerequisites could also learn enough type theory to write specifications in a couple hours because you don't actually need a deep understanding of type theory to use it (though maybe you meant that you immediately started writing specifications of large, real-world systems in TLA+, but I'd presume you'd then be the outlier on that). In my experience people pick up Isabelle (/HOL) really quickly and writing specifications in a type theory based proof assistant isn't a huge jump from that. Now, writing actual proofs is a completely different matter, but I didn't disagree with you on how economical/ergonomic the over all approach actually is, just the basic complexity of the theory/specifications ;) >What is the type of its first argument? Some universe U, which is an implicit argument. You could alternatively write your Lean example as def id {u} {α : Sort u} (a : α) : α := a Not being able to specify the type of u in Lean might seem kinda cheaty, but I'd say that's similar to how one declares generic type parameters in e.g. Java. You wouldn't say that those languages' generic functions aren't actually functions, would you? Similar to how one could make those generics explicit, it is actually possible to define a special type of all universes (not including itself). Agda does this by having a special primitive type of universe levels. As an example id : forall {u : Level} -> forall {A : Set u} -> A is the signature of the universe polymorphic identity function. The Level type doesn't you any issues because it is essentially a 'top' type that doesn't have a type itself.
- pron 6y ago
  > but I really think anybody who has all those prerequisites could also learn enough type theory to write specifications in a couple hours because you don't actually need a deep understanding of type theory to use it That has not been my experience. Typed formalisms have further complications with "partial" functions -- either they're actually partial, which is a rather complex concept, or you need refinement types to define them, as well as with constructive mathematics, which isn't necessary for specification. Plus, what are you going to do with your specifications after a few hours if you can't write proofs after few hours (or a few days)? And because of that the tutorials don't and won't just teach specification first and proof later -- as the TLA+ tutorials do -- so even if this were hypothetically true, you have nowhere to learn things like that. Lean has very good tutorials, and you can compare how far they get how quickly with the TLA+ tutorials. I don't know if it's even possible to teach such formalisms the same way as TLA+, but even if it were possible, I haven't seen such tutorials. Those languages are so infused with their formalism's proof theory that it's hard to separate the two [1]. For example, most typed formalisms define integer division by zero to equal zero. Suppose they didn't, and they wanted to teach how to define division "properly". How much would a student need to know in order to define and use the div function? OTOH, TLA+ handles partiality in what I think is a simpler way, with a careful definition of Hilbert's epsilon operator (see https://pron.github.io/posts/tlaplus_part2#the-choose-operator-and-the-meaning-of-undefined https://pron.github.io/posts/tlaplus_part2#the-choose-operat...) Finally, most specifications people in industry are interested in are not of sequential algorithms but concurrent ones, which you also can't do after a few hours (or a few days). > In my experience people pick up Isabelle (/HOL) really quickly Depends what you mean by "really quickly." Isabelle has some accidental complications such as the nested languages. But I think something like Why3 can be picked up quickly, although it doesn't handle concurrency easily. > Not being able to specify the type of u in Lean might seem kinda cheaty, but I'd say that's similar to how one declares generic type parameters in e.g. Java. You wouldn't say that those languages' generic functions aren't actually functions, would you? The type system in Java or Haskell cannot be used as a sound mathematical foundation, so whatever I call those things it would mean something quite different from maths functions. I call them subroutines, but those that call them functions know (I hope) that they're overloading the term. In any event, students that do learn simply typed lambda calculus learn it in the context of programming languages whose type systems are inconsistent and they certainly don't learn how to do maths with them. Anyway, `id` is not a function in Lean because the universe argument doesn't have a type. But I wonder, in Agda, is `id id` some object even when a specific universe cannot be inferred? If so, how does Agda avoid Russel's paradox? [1]: Which I think is a big problem. The clean separation of model and proof is an important property of a formal logic designed for ease of learning, expression and comprehension, and we must not forget that ease of learning, expression, and comprehension -- so that practitioners rather than logicians will be able to make everyday use of it -- has been a central goal of formal logic since at least Frege, if not Boole or even Leibniz, equal in importance to, if not superseding, that of mechanical proof. I might be getting carried away, but I think that TLA+ is a pretty special accomplishment in the history of formal logic in that it is perhaps the first truly rich formal logic that is commonly used by non-specialist practitioners in their day-to-day work.