Either (and variants thereof) are mostly used in the functional programming world. And I believe Either can be modeled exactly as a (discriminated, precise) union in Avail. (and Option[X], which we already discussed in the past).
Currently, the type union: [1..5] U [10..15] returns the non-precise type
[1..15].
Conversely, Avail does return the exact union: 2’s type U 3’s type.
It would be nice if [1..5] U [10..15] would return [1..5] | [10..15] (in some,
yet to be decided notation).
Here is a contrived example:
Method "random choice between_and_” is
[
a : any,
b : any
|
if a's hash > b's hash then [a] else [b]
];
Semantic restriction "random choice between_and_” is
[
a : any's type,
b : any's type
|
a ∪ b
];
Why shouldn’t we be allowed to exactly type the random choice between a string
and a number?
The issue is that we want to strengthen a return type, based on the argument
types, without collapsing into nontype for non-obvious unions.
Why would we throw away useful type information when there is no need?
(other than compiler woes :))
Here is a less contrived example:
Currently tuples are restricted to have a size less than MAXINT.
Now let’s say we want to implement an object bigtuple (a tuple of tuples), that
behaves exactly like a regular tuple.
class "bigtuple" extends object with fields btuple : <tuple…|2..>;
Abstract method "_++_"is [bigtuple, bigtuple]→ bigtuple;
…
At runtime, we want to use the built-in tuple for a ’small-sized’ tuple,
switching to bigtuple when it exceeds MAXINT, and reverting back to the
built-in when it drops below MAXINT.
(modeled as Either <Tuple,BigTuple> in the Java world).
Let’s call such tuple type “etuple” (extended tuple).
etuple ::= tuple ∪ bigtuple;
Abstract method "_++_"is [etuple,etuple]→etuple;
…
We can always fall back to nontype (like it is now) and leave it to runtime
dispatching, but we want to be as precise as possible at compile time.
All this can probably be achieved through wrapper objects (similar to Either)
but that’s not very (memory) efficient.
cheers,
Robbert.
> On 13 Feb 2015, at 23:07, Mark van Gulik <[email protected]> wrote:
>
>
>
>
> On Feb 13, 2015, at 1:24 PM, Robbert van Dalen <[email protected]> wrote:
>
>> So here is the use case in Java (or something similar):
>>
>> interface Either<A, B> { }
>> class Left<A, B> implements Either<A, B> {
>> public A left_value;
>> public Left(final A a) { left_value = a; }
>> }
>> class Right<A, B> implements Either<A, B> {
>> public B right_value;
>> public Right(final B b) { right_value = b; }
>> }
>>
>> As Avail doesn’t have type parameterisation, how would one model Either in
>> Avail, efficiently and precisely?
>
> I think the part that's missing from this question is what you think you
> should be able to *do* with such a construct. It looks like it implements
> something like a C union (I.e., a struct with overlapping storage), but with
> a tag (like Pascal's variant records). You still have to cast to get the A
> (or the B) out of it, and the Either is directly compatible with neither A
> nor B.
>
> C avoids this difficulty by happily violating its own joke of a type system
> and reinterpreting a section of memory as something that it isn't. Its idea
> of a cast does essentially the same thing, rather than the more modern idea
> of dynamically checking and then strengthening the type of an object (e.g.,
> Java — C++ is not modern, and has neither objects not sincere types).
>
> If you want to have the equivalent functionality in Avail, you can type
> something as any, then cast it to a stronger type when you believe it to be
> of that type. It doesn't need a separate tag, since an object always knows
> its own type. The simple form of casting is the question-mark right-arrow
> operator (which raises an exception). Or you can throw an "else[do
> something]" clause on the end.
>
> If you want to tie it to mutability, just create a variable of type any, and
> pass that around instead.
>
>> Dare I say precise union types?
>> Yes!
>
> Precise union types will be a slightly different beast. [1..5] U [10..15] U
> catfish will be a valid supertype of, say, [10..15], but not of [9..15]. But
> you can only use an expression of this type where something at least that
> general is expected, which means you can't do arithmetic with it unless you
> strengthen it, nor can you fry it in lemon juice, butter, and dill unless you
> strengthen it a different way.
>
>
signature.asc
Description: Message signed with OpenPGP using GPGMail
