zarakshR

I don't see how:

Racket:

  > (define (fact n)
      (if (= n 1)
          1
          (* n (fact (- n 1)))))
  > (fact 6)
  720

OCaml:

  # let rec fact = function
      | 1 -> 1
      | n when n > 1 -> n * (fact (n - 1))
    in fact 6;;
  - : int = 720

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 point is you can't simply treat non-nullable as a subtype of nullable in general, because this case exists.

But surely, you can still use subtyping in other cases -- when it is already unboxed -- right?

Like so: `T <: T?` for all boxed `T`.

> 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.....

Continuation-passing style?

> 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.

Peak HN.

How would that even work if git was released in 2005? Am I missing something?