From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x33e.google.com (mail-ot1-x33e.google.com [IPv6:2607:f8b0:4864:20::33e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id f8cf8032 for ; Tue, 12 Feb 2019 15:59:43 +0000 (UTC) Received: by mail-ot1-x33e.google.com with SMTP id o13sf2980172otl.20 for ; Tue, 12 Feb 2019 07:59:43 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=HV1+49QwyqrIWoHKfXPpc5JNSs0Vq1AYknKwUPFtPng=; b=PbYTpyvPEJMtmw5FMyRG00rHZnHM+LniFjtr2TWElzSXwI/GYgbW5gLlkoIYx4IfNb hvQkGgd+OJlH6BOCCCYfJanf4j7Lw+jLEg2EsB1LxQtSWl8hmUtXKZDTyqLuB6Phb/RB 6VyYTZr0l5UF076PZV4FBvIqQ4KCpS9JhJS2yttbzQU4L8f5eT96GCj2FLeYE0kuDdVt bJ9rl6faXn1tOO90lSyL/29P+xBMh5UHb+FkHg2KEUKzISLXn9WO5sC9GxpAHLdASsj1 AKkclBbPIT4kjdNBt3CUk+DQv+RZp+joff/wVekuQIYg50jQ/tCsal3Ouy8jQvlU17si EbNg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=HV1+49QwyqrIWoHKfXPpc5JNSs0Vq1AYknKwUPFtPng=; b=rX+f6cr39V8qIqSNBucZn0fLnrmR31NxgwOpiT7PkNCB8F8ct1711wvNpc1esT6al4 aXt2a7Pg9Z6rrGUh7WO+CZgB8ZCBbx9PWO+QeX8Gcll9qX1WL+rxNlKiwzjUhVJwYUIh mbAyCPufRnjTOGUnHSfpOYkOYRAGW8wbeHQbWM3b/GxPZQk6+/q3WD5LoqArgNXnjJAf XPxzorURu1IbEvnWmLbd08zfWFJjT9+BFuy7XjZc8wdbJRCfoBwt8kiC4aYk7tLRsnzT eekSTEyXtnXhARW9Fd68yi2zgrW3kR1GsIMbd2kRdOsxkmexw60rZg4LsXfsBA98THty qHDw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=HV1+49QwyqrIWoHKfXPpc5JNSs0Vq1AYknKwUPFtPng=; b=oHMzcFwNkJGLaCmf1BpXlTTg0bOtKngBwLN8iik/jjveYluAMJ6UFNILb/GJKqj+bq LsCKrgJp+pMjHv6dbO0Ydh10BwF/4mKGEWRtthDdrVYCj5uNDPVywio4JCMpENIF3c37 LmXylb5rhxd6MDXJdpc5yMV6co2vr9HS5EKgTTYHeXleK+g8dEhaBCUGRXo481CU/mW7 uqw+5dPxP1MfR959ZATYySDHC7bxUwFJGQjkqNgKEx9so9WuZb24eTEjgqbuuRv581JA /DxwsVJ9zn2ccTDiXpOxMAlBoOAvWR6umZfB10n4hqypUzqu1ZQ8HxGDNqhobKLnPUVF RCLQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuaFnvdp4zYr0QwI0wzhgoLLfQ4G07nTvvU5YwUgaAo0Kinlb+P6 rMMlVwlRUbRajrOEIIx8gV4= X-Google-Smtp-Source: AHgI3Ia/Rqn/Vfbp8UJD7Tt9POv7yQ2NjyT1mP25+80Hr3Uo9tw+OPx5l3dHvSVC7gHQz9ARvusYdw== X-Received: by 2002:a54:4d86:: with SMTP id y6mr1333oix.0.1549987182413; Tue, 12 Feb 2019 07:59:42 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:6409:: with SMTP id h9ls10718107otl.8.gmail; Tue, 12 Feb 2019 07:59:42 -0800 (PST) X-Received: by 2002:a9d:da3:: with SMTP id 32mr111554ots.3.1549987181918; Tue, 12 Feb 2019 07:59:41 -0800 (PST) Date: Tue, 12 Feb 2019 07:59:41 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: In-Reply-To: <6C0820F2-A1E7-412B-A008-51FCF62BA257@nottingham.ac.uk> References: <2b86e469-309d-4a7a-8ad0-d7a0cb376c74@www.fastmail.com> <3d0f6986-0136-480f-8c01-b593cbe3fff9@googlegroups.com> <84a7fbdf-aa40-4d4e-a3f7-1285f1171625@googlegroups.com> <2CD19190-1CC2-4B74-AAEA-C0DCAB6B1019@exmail.nottingham.ac.uk> <8ab48f34-edd7-4ed3-bc35-526bd8d10562@googlegroups.com> <6C0820F2-A1E7-412B-A008-51FCF62BA257@nottingham.ac.uk> Subject: Re: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_68_314077255.1549987181390" X-Original-Sender: atmacen@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , ------=_Part_68_314077255.1549987181390 Content-Type: multipart/alternative; boundary="----=_Part_69_341303453.1549987181391" ------=_Part_69_341303453.1549987181391 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Tuesday, February 12, 2019 at 10:36:08 AM UTC-5, Thorsten Altenkirch=20 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= =20 you don't have to use. You would only need to understand the object-based= =20 semantics of types to fully understand the language. Why do I have to capture all possible constructions if I just want to talk= =20 > about some specific ones? > I don't understand this. This is something that irritates me about set theory: if I want to say for= =20 > all natural numbers =E2=80=A6, I am actually saying for all sets which tu= rn out to=20 > be natural numbers=E2=80=A6 At least conceptually this is rubbish. Who th= inks like=20 > this? > This doesn't seem to have anything to do with Nuprl. In Nuprl, saying for= =20 all natural numbers is a Pi type with domain nat, as usual. Yes and in computer science we think about types sorting untyped programs.= =20 > 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= =20 out to be much harder than understanding computation on its own,=20 operationally. Before denotational models, the untyped lambda calculus was= =20 already well-understood operationally. Scott deepened our understanding of= =20 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=20 > easier to understand, they make sense by themselves so lets refer to them= .=20 > Yes we implement them based in intyped things, trees, strings, bit=20 > sequences but we don=E2=80=99t need low level concepts to understand high= level=20 > 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=20 about the implementation of typed elements in terms of untyped or=20 less-typed objects. This is refinement typing, and it's not just Nuprl vs= =20 the world. --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_69_341303453.1549987181391 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Tuesday, February 12, 2019 at 10:36:08 AM UTC-5, Thorst= en 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 t= o understand the object-based semantics of types to fully understand the la= nguage.

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 =E2=80=A6, I am actually saying = for all sets which turn out to be natural numbers=E2=80=A6 At least concept= ually this is rubbish. Who thinks like this?


This doesn't seem to have anything to do with Nuprl. In Nuprl, s= aying for all natural numbers is a Pi type with domain nat, as usual.

Yes and in computer science we think about types sor= ting untyped programs. But why?


Some c= omputer scientists like untyped programs.

Do you understand the untyped lambda calculus?=


Yeah, I'd say so.

It took Dana Scott a while t= o come up with a mathematical semantics.

<= br>Because understanding this connection between computation and math turne= d out to be much harder than understanding computation on its own, operatio= nally. 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 le= ts refer to them. Yes we implement them based in intyped things, trees, str= ings, bit sequences but we don=E2=80=99t 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 us= ers reason about the implementation of typed elements in terms of untyped o= r less-typed objects. This is refinement typing, and it's not just Nupr= l vs the world.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_69_341303453.1549987181391-- ------=_Part_68_314077255.1549987181390--