Re: [OFFTOPIC] Re: Appending lists

[Eduardo Ochs]

On Fri, 18 Jun 2021 at 21:06, Emanuel Berg via Users list for the GNU
Emacs text editor <help-gnu-emacs@gnu.org> 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