From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Eduardo Ochs Newsgroups: gmane.emacs.help Subject: Re: [OFFTOPIC] Re: Appending lists Date: Fri, 18 Jun 2021 22:20:53 -0300 Message-ID: References: <4tl1yvylvg1fxx5eefjs9mnk.1623688568572@email.android.com> <87o8c8l32h.fsf@posteo.net> <87zgvs2bup.fsf@zoho.eu> <87y2bby1kr.fsf@zoho.eu> <20210615091834.GB24886@tuxteam.de> <87im2ewr3k.fsf@zoho.eu> <20210616072819.GB17919@tuxteam.de> <20210616151101.GB5669@tuxteam.de> <875yydtnqz.fsf@zoho.eu> <87im2a3ek5.fsf@zoho.eu> Mime-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="6645"; mail-complaints-to="usenet@ciao.gmane.io" To: Emanuel Berg , help-gnu-emacs Original-X-From: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane-mx.org@gnu.org Sat Jun 19 03:21:38 2021 Return-path: Envelope-to: geh-help-gnu-emacs@m.gmane-mx.org Original-Received: from lists.gnu.org ([209.51.188.17]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1luPg1-0001Ye-Tj for geh-help-gnu-emacs@m.gmane-mx.org; Sat, 19 Jun 2021 03:21:37 +0200 Original-Received: from localhost ([::1]:43280 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1luPg0-0004Kx-D3 for geh-help-gnu-emacs@m.gmane-mx.org; Fri, 18 Jun 2021 21:21:36 -0400 Original-Received: from eggs.gnu.org ([2001:470:142:3::10]:50158) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1luPfY-0004K6-Un for help-gnu-emacs@gnu.org; Fri, 18 Jun 2021 21:21:09 -0400 Original-Received: from mail-pj1-x102a.google.com ([2607:f8b0:4864:20::102a]:54222) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1luPfX-0008Li-CO for help-gnu-emacs@gnu.org; Fri, 18 Jun 2021 21:21:08 -0400 Original-Received: by mail-pj1-x102a.google.com with SMTP id bb20so2545535pjb.3 for ; Fri, 18 Jun 2021 18:21:07 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to; bh=CmOylTYa9OcE2A+AQ9u9bKCXw+H+Vli6rJ0UO7cj4E0=; b=c4ym3UrtZuKmCUuAIFzYN/DAdWBmh+RTEvlw+oV6m/rsqYrOh9bFxpssBOA+RRlryN RdhcgG/UVZTqeDxcZD4uqzaN2AIQ1MIFNu6j6LmqQu/T/7WnVZd93PbltyyX4Of+cbRr /6Er/tRWRjNobDBfGoSuuW2sDqmKciv6qVfKUau1inioKim40hE61/ApNerSCG8QDptW U0ELctxysze6H/TTRQKj+FQWN6GJriSkxGZz2dYLt8Dq6nC2Gv2ZW8vkcFySA/OFoJtv T4REC4mAMmfs3HWQSLIIYMLbqQwJCA/0VZD1RtJMsqkFlW2L8TRIuVN0kVKRz/vPJ441 cZvw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to; bh=CmOylTYa9OcE2A+AQ9u9bKCXw+H+Vli6rJ0UO7cj4E0=; b=CA+zOq4XgvY4UOe8V8+++Ju2PeftX2RhGlsCw10Oscllo3+m3SVEa2l69gAtzoknyF brszwd2CxsHhDrAct6EMxi2D+ajxS4ZRUHf1Qeobbexn72IqHrqEhtMEN/CHe0uXBDDT p0wbHyZuife8yOudmLkql3lr0eYnX5rfCfJpFEXNZ51xwCtj1KpKtGfgJgVYneiU5u8a vPyNOYs5RpSTGm9jKIp3rcpFmQthJlmhayV2kwXTgfm19xNCq6BSAX/uOMSQjaqwdMDU PvCijX1KDuu5/7hNm2R2+fH58ALFy4YQjWCTP0CiE1tqybB9VcyMhri4praDOYLusx4V j7FQ== X-Gm-Message-State: AOAM5312AimNxMbmSBce0VL2sJjOwe1B7XkhBrULO5q3Dfdr//8Eumee I/ZNPkBk1cP7BPrWqck8Qitfg0UIQrQ9Iqn7F0k= X-Google-Smtp-Source: ABdhPJyvNh8p2Cb9vfenKrkf3EMECPLNwQpcnm6jRVybe2S5ZLmpxyro8MH1RjKMhChthF++TP2ok1PtqcN05yxFgVk= X-Received: by 2002:a17:90a:aa05:: with SMTP id k5mr24491348pjq.117.1624065665728; Fri, 18 Jun 2021 18:21:05 -0700 (PDT) In-Reply-To: <87im2a3ek5.fsf@zoho.eu> Received-SPF: pass client-ip=2607:f8b0:4864:20::102a; envelope-from=eduardoochs@gmail.com; helo=mail-pj1-x102a.google.com X-Spam_score_int: 0 X-Spam_score: -0.1 X-Spam_bar: / X-Spam_report: (-0.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001, RCVD_IN_DNSWL_NONE=-0.0001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, URI_DOTEDU=2 autolearn=no autolearn_force=no X-Spam_action: no action X-BeenThere: help-gnu-emacs@gnu.org X-Mailman-Version: 2.1.23 Precedence: list List-Id: Users list for the GNU Emacs text editor List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane-mx.org@gnu.org Original-Sender: "help-gnu-emacs" Xref: news.gmane.io gmane.emacs.help:131004 Archived-At: On Fri, 18 Jun 2021 at 21:06, Emanuel Berg via Users list for the GNU Emacs text editor wrote: > > Stefan Monnier wrote: > > > https://www.quantamagazine.org/does-time-really-flow-new-clues-come-from-a-century-old-approach-to-math-20200407/ > > > > [ The relationship being that type theory is generally > > associated with constructive logic rather than with > > classical logic. ] > > Eh, "type theory"? Are we talking types like in > a programming language? There is a theory behind that? > > I always thought it was just a matter of arranging 0s and 1 in > a way that was agreed-upon locally to denote that something is > something so it can be recognized and operated upon/used in > certain ways? > > Much like a network communication protocol. Like question one, > what does the messages look like (how are they organized)? > Question two, in what order are they supposed to come? > Question three, what does it all mean? > > And that's it? > > Well, maybe there is a theory to networks as well, now that > I think about it. Of course there is. Bad example. But that > still feels more theoretic than types, with node diagrams and > stuff... Hi Emanuel, take a look at Benjamin Pierce's "Types and Programming Languages" - https://www.cis.upenn.edu/~bcpierce/tapl/ and at Chapter 1 of the HOTT book: http://saunders.phil.cmu.edu/book/hott-online.pdf Cheers, Eduardo Ochs http://angg.twu.net/#eev