6 ms·

>In the time in took me to grasp Lean's type-theoretic universal quantification I'm not sure what you mean? They work in the exact same manner as in normal pre

• pron 6y ago
  > They work in the exact same manner as in normal predicate (higher order) logic. It is based on dependent products which you need to understand sooner-or-later (sooner, really), and are rather more intricate than FOL. > Uh, are you talking about the normal identity function? 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). In TLA+ the meaning of terms is simpler, as there is a clear distinction between pure syntactic operators and domain objects (sets, but also functions). So in TLA+, you can have either: Id(x) ≜ x which is just parameterised syntax that does not denote any domain object, or perhaps you'd want: Id(S) ≜ [x ∈ S ↦ x] which is an operator defining the identity function on a given set. In Lean, however, universe u def id {α : Sort u} (a : α) : α := a which is similar in spirit to the second TLA+ definition, describes a rather complex object in the meta-domain.
  • ImprobableTruth 6y ago
    >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.