Re: [OFFTOPIC] Re: Appending lists

[Stefan Monnier]

>> [ 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?

You might also want to start with

    https://en.wikipedia.org/wiki/Type_theory

What you're thinking of is usually called "(computational) type systems"
instead, as in

    https://en.wikipedia.org/wiki/Type_system

As the first says:

    Type theory is closely related to, and in some cases overlaps with,
    computational type systems, which are a programming language feature
    used to reduce bugs.


-- Stefan