[Grace-core] Minutes of Telecom 17-18.5.2012

[James Noble]

> "unit"?

so if we do that, we'd write "unit" I guess...
(Andrew is the fan of Post-Ascii notations;
 I've noticed that every time I put something
 past character 127 on a slide, I always get
 a question about "how do you type it in?"

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

sure ...

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

Hmm, certainly from my GCC days, marking out non-returning calls
is definitely useful.

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

Ok right...

>> 
>> 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"?

right.  NoValue? 

>> 
>> * 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)),

right...

> and bar to return a number (i.e. to have Number as its return type).

sure - there is a question as to whether we infer & bind return types or not.
I think it comes in mostly when we are checking subclasses (which we probably
don't do right yet)

> The following baz and quux would not return:
> 
> method baz { baz }
> 
> method quux { FrobException.raise }

right

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

fair enough.

>> 
>> 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 :-)

yes, you're right there - whereas the "noSuchValue" (still would like a less clumsy name)
will be needed once you start writing types for "void" methods...

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

right.

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

so we do have a trap value "uninitialized" for, well, uninitialized.
just reading that out of a variable causes and exception.
For none, though we do need to be able to return it, at least,
and i think pass it around too,  because otherwise wer'e not
as polymorphic as we'd like to be (although that polymorphism,
proper function vs command, isn't something functional languages need).

language design is fun!

James