On 31 October 2016 at 13:32, Waldek Hebisch <[email protected]> wrote:
> Bill Page wrote:
>>
>> On 28 October 2016 at 22:16, Waldek Hebisch <[email protected]> wrote:
>> >
>> > BTW2: The desion goal of FriCAS typesystem was that answer
>> > to questions like 'sameType?' should be mostly statically known,
>> > without need for runtime tests (I write "mostly" because
>> > Union-s require some testing).
>> >
>>
>> What testing is required for Union? For example if
>>
>> x:Union(Integer,Float)
>>
>> then the static type of x is just 'Union(Integer,Float)' for ALL
>> values x. Whether we can produce a given value by coercing
>> an Integer or a Float is not part of the type information, is it?
>
> Formally type of 'x' is just Union, so you are right that no
> dynamic checking is needed to know static type of 'x'.
> OTOH branch of union is part of type information:
I find that I disagree with you on a number of points and I think that
FriCAS unfortunately inherits a poor design and confused
implementation of Union from Axiom. This is an example of what I meant
in another message by how the lack of a good general theory leads to
ad hoc solutions and ultimately to under-utilization of important
language features.
The possible branches of Union are entirely analogous to the
components of Record. Both branches and components have associated
types but they are not types themselves. Record and Union (also called
Variant or tagged-Union) are dual concepts called Product and Sum
types. Untagged-Union in Axiom is just a shorthand for a common
use-case where the associated types of each branch are all different
and branch labels are therefore redundant.The actual branch for a
value of type Union is part of the value, not part of the type.
> Spad compiler will allow coercion of 'x' to Integer only if
> you earlier checked that 'x' can be coerced to Integer.
> Pragmatically, 'x case T' is used in places where other
> systems may have dynamic type checks.
'T' is a branch label, not a type. It only looks like a type in the
case of untagged-Union. In the general case one can write for example:
(1) -> x:Union(integer:Integer,float:Float)
Type: Void
(2) -> x:= [3.0]
(2) 3.0
Type: Union(float: Float,...)
(3) -> if x case float then x.float
(3) 3.0
Type: Float
where the lower case symbols are just branch labels not types. No
coercion is involved at all. We just need to choose a branch.
But this is still confused because the interface for unlabeled Union
is unnecessarily different from the labeled case and because of an
inappropriate use of construct [ ] operator. The label symbols of
Union should be exported as value constructor (injection) operators.
In the example above, having signatures
integer: Integer -> Union(integer : Integer, float : Float)
float: Float -> Union(integer : Integer, float : Float)
Then we could just write:
x := float(3.0)
where the type of 'x' is already known. Moreover the following is a
sensible Union type
x: Union(f1 : Integer, f2 : Integer)
but Axiom does not provide an interface to unambiguously create values
for this type because the 'construct' operator is overloaded and
depends on function selection based on the associated type of the
branch.
Finally Enumeration is a degenerate form of Union where the associated
type is completely unnecessary
x : Union(f1 : Void, f2 : Void)
x := f2()
if x case f2 then ...
but instead Axiom implements this with a peculiar syntax
Union("f1", "f2")
> To put it differently, static typing alone will not eliminate need
> satisfied by type checks in dynamically typed language.
The branch labels in Union are an inherent part of the logical
structure of a program. Nothing prevents a dynamically typed language
from implementing Union this way.
> Of course some type checks are just result of poor program
> organization. Many type checks will go away due to overloading.
> But there is important class of type checks that can not
> be easily eliminated. In such cases tests using 'case'
> may do.
The proper use of Union can lead to better program design but this
really has nothing to do with type checking.
> Or as last defence one may be forced to use 'Any'...
>
'Any' is appropriate in some applications but I do not see why it
should be viewed as a "last defence" against anything.
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.
