On Tuesday, February 12, 2019 at 10:36:08 AM UTC-5, Thorsten Altenkirch wrote: > > Why do I need to understand objects to understand elements? > As a user of Nuprl, you don't. Objects give you a new way to reason, which you don't have to use. You would only need to understand the object-based semantics of types to fully understand the language. Why do I have to capture all possible constructions if I just want to talk > about some specific ones? > I don't understand this. This is something that irritates me about set theory: if I want to say for > all natural numbers …, I am actually saying for all sets which turn out to > be natural numbers… At least conceptually this is rubbish. Who thinks like > this? > This doesn't seem to have anything to do with Nuprl. In Nuprl, saying for all natural numbers is a Pi type with domain nat, as usual. Yes and in computer science we think about types sorting untyped programs. > But why? > Some computer scientists like untyped programs. Do you understand the untyped lambda calculus? > Yeah, I'd say so. It took Dana Scott a while to come up with a mathematical semantics. > Because understanding this connection between computation and math turned out to be much harder than understanding computation on its own, operationally. Before denotational models, the untyped lambda calculus was already well-understood operationally. Scott deepened our understanding of it, and of general recursive types more generally. It's not all or nothing. I think we should put our mouth where our heart is. Typed objects are > easier to understand, they make sense by themselves so lets refer to them. > Yes we implement them based in intyped things, trees, strings, bit > sequences but we don’t need low level concepts to understand high level > concepts!! Yes we need them to implement them but this is another issue. > I truly believe that it's useful for the type system to let users reason about the implementation of typed elements in terms of untyped or less-typed objects. This is refinement typing, and it's not just Nuprl vs the world. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.