[Grace-core] Minutes of Telecom 17-18.5.2012

[Bart Jacobs]

On 22/05/2012 11:31, James Noble wrote:
>> Apologies if I'm belaboring the obvious...
> no it's all fine, and it's good for us to be clear about our motivations for things.
>
>>   '()', or 'tt
> we thought about these, and one question was "how do you pronounce them?"

"unit"?

>
>> Also, it would be useful to have a type Nothing that truly has no values. This would be the return type of methods that never return, like exit. This informs the type checker that subsequent code is unreachable, so that it doesn't complain about missing result values etc.
> that's a good point - I don't know if Nothing is the best name for it, rather than
> NeverReturns or something?  NoExit?

Note that it might be useful in other circumstances as well. For example:

type SumType<A, B> = {
     method get: A | B
}

If you call 'get' on something of type Sum<Number, Nothing>, you know 
you're going to get a number.

I can't think of any other important examples right now, but I do 
remember using Scala and being impressed by the power of Nothing.

BTW: OCaml has a similar feature. If the type inferencer can infer that 
the type of something is "forall 'a, 'a", then it knows that that code 
point is unreachable since there is no value of that type. So, the type 
of "raise" in OCaml is "exn -> 'a".

>
> the big problem with the name "Nothing" is that in Grace you can write nothing*
> instead of a type - if you just leave the type out, you get type Dynamic* on inputs,
> or an inferred type on outputs.   But writing the world "Nothing" means something
> rather different than writing "" nothing.    See - it's even hard to write about!

I guess Void would also be a bad name, since in C-like languages, "void" 
actually means "Unit", not "Nothing" (in Scala terms). "Empty"? "NoValues"?

>
> * we could be pickier here, distinguishing between writing no type annotation
>
>         method foo(x) {z := x}
>
> or writing an annotation that itself is the empty string
>
>         method bar(x :) ->  {x + x}
>
>
> so e.g. bar could mean "returns noSuchValue"   (or noUsefulValue)
> while foo's return type could mean "does not return"

(Did you check the method bodies? One would expect foo to return the 
non-useful ("unit") value (i.e. to have Unit as its return type (in 
Scala terms)), and bar to return a number (i.e. to have Number as its 
return type). The following baz and quux would not return:

method baz { baz }

method quux { FrobException.raise }

They would have Nothing (in Scala terms) as their return type.)

>
> but, again, we figured that was a distinction that would be very hard to explain.

Yes. In any case, I think the empty type (Nothing in Scala) would not be 
used so often that it deserves special implicit syntax, and in fact 
would be used so rarely that it deserves a very explicit calling out of 
its name :-)

>
>> Update: The penny drops :-) Of course, None refers to Some|None, the option type. Yes, that makes perfect sense. Sorry for being slow :-)
>
> Umm, I think so?    in Grace we're untagged, so we'd do   e.g. String|None
> (or, if noSuchValue is self matching, we have the option of String|noSuchValue)

Yes. Makes a lot of sense.

> Although I do recall a discussion saying we didn't want noSuchValue to actually
> *be* a useful null...  (e.g. perhaps it doesn't even understand == or something)

That sounds like a 'trap value' of some kind. Touch it and you die. (The 
C standard allows uninitialized variables to hold trap values.) There 
may be room for both. In any case, a well-behaved "None" value seems to 
have proven its usefulness in functional programming.

Bart


Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm