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