This is not relevant since this de-sugaring cannot be performed if `name` is recursive (i.e., if `term` refers to `name`), which `Y` is. So the author's derivation is still required in the pure lambda calculus.
> because PHP and Javascript will implicitly convert back and forth
If you can provide (valid!) methods `T -> U` and `U -> T` for two types, why wouldn't `T = U` hold? (Atleast for types where `=` makes sense)
This is the definition I am using:
> S is a subtype of T, written S <: T, if a value of type S can safely be used in any context where a value of type T is expected.
from Pierce's "Software Foundations"
Of course, you may not want to make `String <: Number` and `Number <: String` (and thus `String = Number`), because there is no sensible way to do so; but this is an issue with the way PHP/JS handles subtyping, not with the notion of subtyping itself and certainly does not apply to the example of nullable types.
Unfortunately, I am not familiar enough with C++ to comment on the other question, sorry!
> The language can just have an implicit conversion rule for convenience
the presence of an implicit conversion rule `T -> T?` amounts to the observation that `T <: T?`, where <: is the subtyping relation
> make an unboxed integer nullable ...
I don't think any language allows this, in any case disallowing nullability for unboxed types amounts to the observation that `P !<: P?`, where !<: is "does not subtype"
I believe (unless I have misunderstood you) that both your examples are subsumed (heh) by subtyping
Similarly, I was shocked to learn that models of aeroplanes don't even account for the possibility of the plane being blown up mid-flight by a stray anti-air missile.
It seems aerospace engineers are just like priests and counselors in the courts of ancient kings.....
> If I am in my normal raw intellect, I will begin going deep on some topic thats outside the range of normal human discourse. It will be hard for me to stop, because of my interest. Alcohol removes that to a large degree.
Racket:
OCaml: