Re: How to make cyclic terms (Was: A miraculous match?)

I didn't make any statements about System F.
When I wrote something doesn't use System F,
then this is based on the observation that
this something doesn't use variables ranging
over types. At least not in the way this
is allowed in System F, namely in System F it
is allowed to form a type that universally quantifies
a type variable. There is a very big Zoo
of type systems, which can be organized by
Henk Barendregt Lambda cube:
https://en.wikipedia.org/wiki/Lambda_cube
"Simple Types" and "System F" are only the
corners λ→ and λ2.
Mild Shock schrieb:

 Maybe you are so simple minded, that
you don't anderstand that "simple" is
essential in forming the technical term:
 "simple types"
 We call "simply types" not because we want
to highly that we think they are "simple".
Its simply that "simply types" is a terminology
 in its own just like "natural numbers" or
"simgular matrix". This is called compound
term formation:
 https://en.wikipedia.org/wiki/Compound_%28linguistics%29
 Do you get it now? Or still not getting it?
 Mild Shock schrieb:

>
You are a fucking moron. You can even
not separate a dozen terms. Its relatively
simple to tell the things appart:
>
- Simple Types ( λ→ )
The simply typed lambda calculus λ→, a form of type theory,
is a typed interpretation of the lambda calculus with only
one type constructor → that builds function types.
https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
>
- System F
Whereas simply typed lambda calculus has variables
ranging over terms, and binders for them, System F
additionally has variables ranging over types,
https://en.wikipedia.org/wiki/System_F
>
Whats so difficult for you moron to understand?
>
Julio Di Egidio schrieb:

On 09/01/2025 17:05, Mild Shock wrote:
>

I told you a dozen times that the scope of
this thread is simple types.

>
Define scope and thread.
>
You are simply a waste of time.  (EOD.)
>
-Julio
>

>