Comment by barkmadley | Hacker News Reader

Comment by barkmadley | Hacker News Reader

Parent Full thread

I assume this is the implementation [1](took me a while to find the type to see how the compiler might interpret it).

I read the definition as (ignoring the implementation):

    return a Value or Absent when given an Iterable<Value,Absent> where Value is Comparable and Absent is Null

Correct me if I am wrong, but there doesn't appear to be anything linking the nullability of the return value based on the possible emptiness of the input value. How does the compiler check this constraint (which sounds a lot like a dependent type relation)?

Upon further reading of the Iterable type[2], I have more questions, does "Nothing" satisfy "Null"?

| If not, then it looks to me like passing in a non-empty iterable (Iterable<X,Nothing>) is a type error.

| If so then I would imagine that it becomes harder to enforce the constraint, likely because the return type can still be Null regardless of input restrictions. Does this use extra type inference on the expressions inside the function to do the enforcement, for instance using the "exists" operator to perform type set subtraction between {Value|Null} and {Null} on the true branch. This implies that if I re-write the max function to have a single exit point (`ret = Null; if (exists values.first) { ...; ret = ...; } return ret;`) then I don't get the same guarantees?

Also the fact that Null is referenced by the "exists" operator also implies that it is part of the language specification, and not actually definable in any meaningful way as a user type.

Digging a bit deeper, I was very disappointed to read this snippet [3]:

    Nothing is considered to belong to the module ceylon.language. However, it cannot be defined within the language.

If I read correctly, that means that I cannot implement the same behaviour/enforcement with completely user defined types.

[1]: http://modules.ceylon-lang.org/repo/1/ceylon/language/1.0.0/...

[2]: http://modules.ceylon-lang.org/repo/1/ceylon/language/1.0.0/...

[3]: http://modules.ceylon-lang.org/repo/1/ceylon/language/1.0.0/...

> Correct me if I am wrong, but there doesn't appear to be anything linking the nullability of the return value based on the possible emptiness of the input value.

Sure there is. The second type parameter of Iterable encodes that, see the definition of Iterable.

> does "Nothing" satisfy "Null"?

Of course. Nothing is the bottom type, it satisfies every type.

> If so then I would imagine that it becomes harder to enforce the constraint, likely because the return type can still be Null regardless of input restrictions.

I don't know what you mean by this. An Iterable<X,Nothing> cannot return Null from its first attribute. Check the declaration of Iterable.first.

> Does this use extra type inference on the expressions inside the function to do the enforcement, for instance using the "exists" operator to perform type set subtraction between {Value|Null} and {Null} on the true branch.

Approximately correct. But "exists" is not type subtraction, it's intersection with the class Object. Cool, huh?

> This implies that if I re-write the max function to have a single exit point (`ret = Null; if (exists values.first) { ...; ret = ...; } return ret;`) then I don't get the same guarantees?

I don't follow. You can't rewrite the function to do anything unsound because the compiler won't let you. Our type system is sound.

> Also the fact that Null is referenced by the "exists" operator also implies that it is part of the language specification, and not actually definable in any meaningful way as a user type.

That's not correct. Go and check the definition of Null. It's just a regular class, as advertised. There is no special behavior defined in the language spec. Sure, the exists operator is defined by the language spec to mean "is Object", but that's just trivial syntax sugar.

I guess the problem here is that you're used to languages full of weird special cases and ad hoc behavior. Ceylon is not like that. Ceylon's type system is very simple and these fancy constructs are layered over it as pure syntax sugar. It's a very different approach to other languages. But in the end it's much more satisfying. You'll just need a little mental adjustment to get used to it.

> If I read correctly, that means that I cannot implement the same behaviour/enforcement with completely user defined types.

Wha?! Nothing is the bottom type! The empty set. You want to define your own bottom types? That's not possible (nor desirable) in any language I know of. There's just no reason why you would want to write a class with no instances.

> I don't know what you mean by this. An Iterable<X,Nothing> cannot return Null from its first attribute. Check the declaration of Iterable.first.

This made me sad again[1], but then this made me happier[2] (internalFirst implied it is defined in the compiler, finding all of the pieces that make up the definition was a bit of a pain since it is dispersed across so many files), but I think I didn't fully understand union types (and that Nothing was bottom) when I wrote the grand parents logical conclusions.

    :t Iterable<X,Nothing>.first ==>
       X|Nothing ==>
       X (because union with empty is an identity)

therefore inside max, the variable first will have type X when given an Iterable<X,Nothing>.first. I also see how it cannot be re-written as I proposed because there is no guarantee that Absent will be of type Null.

> That's not correct. Go and check the definition of Null. It's just a regular class, as advertised. There is no special behavior defined in the language spec. Sure, the exists operator is defined by the language spec to mean "is Object", but that's just trivial syntax sugar.

I did check the definition of Null, I was merely pointing out that although it is a user definable type, the language specification does mention its existence here[3] and here[4] which is where I looked to try to find out what the "exists" keyword meant. Specifically:

    in the case of an exists condition, a type whose intersection with Null is not exactly Nothing and whose intersection with Object is not exactly Nothing, or

Later on it says "exists x is equivalent to is Object x, and..." but then why reference Null earlier?

> I guess the problem here is that you're used to languages full of weird special cases and ad hoc behavior.

While I thank you for your time answering my mis-understandings of union types, please do not shoe horn me. My main programming activities are using OCaml and Haskell, both of which have very few ad-hoc language features, if any.

[1]: http://modules.ceylon-lang.org/repo/1/ceylon/language/1.0.0/...

[2]: https://github.com/ceylon/ceylon.language/blob/master/src/ce...

[3]: http://ceylon-lang.org/documentation/1.0/spec/html_single/#c...

[4]: http://ceylon-lang.org/documentation/1.0/spec/html_single/#a...

> I was merely pointing out that although it is a user definable type, the language specification does mention its existence

Sure, the language spec _mentions_ Null, in order to define the syntax sugar X? and exists x. But that doesn't mean that Null has any special place _in the type system_.

> My main programming activities are using OCaml and Haskell, both of which have very few ad-hoc language features, if any.

OK, great, sorry for making assumptions. In my defense, I just didn't quite understand why you were having such a hard time believing that Ceylon could do things like this without adhoc special cases.

Reply on news.ycombinator.com