Re: Seeking for papers about tagged types vs access to subprograms

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Wed, 8 May 2013 15:27:50 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:nd22gfeezrwf$.tlj4yyygrwq3$.dlg@40tude.net...
> ...
>> Each time you do something with a type you get another one. Otherwise it
>> becomes untyped.
> 
> That way leads to madness, I think. It's better for "types" to be fairly 
> weak and interoperable.

Weak typing is better?

> In this model, "types" are the low-level view of 
> entities (with things like representation, "kind" [integer, float, array, 
> etc.]).

Structured type equivalence, DDL, the third manifesto etc.

> On top of that, you have some thing else, let's call them "profiles" 
> (as "interfaces" imply dynamic behavior, which is not what we're talking 
> about here). In my language, "profiles" are statically checked and apply to 
> objects as well as subprograms (objecting being overloadable). "Profiles" 
> provide the high-level view of entities, and would be where properties like 
> "apples" and "oranges" would be dealt with. There'd be a shorthand for 
> adding a profile to all uses of a type (just as subtypes provide that for 
> constraints in Ada). If the profiles "match", then the items are compatible, 
> and if they don't, then they're not.
> 
> If done right, this would provide a lot more static checking opportunities 
> than Ada could ever have, and it would get away from the stale notion of 
> "type", which is just not powerful enough by itself.

This, I am afraid, is how many people view strong typing and how this leads
them away from typing. It takes certain courage to admit that you hate
strong typing, because it became a sort of PC-doctrine, which everybody
feels obliged to commit publicly to, while cursing it privately. Still the
alternative to strong typing is the horrific mess you just have described.
Of course I completely disagree with your view. 

Strong typing is madness only without type hierarchies. Types are not
isolated. In certain contexts values of different types are
interchangeable. E.g. Positive can be used as Integer in some contexts. In
other contexts it cannot. This difference makes them distinct types,
nothing else. Where is a difference there is a new type. Substitutability
(= implicit type conversion) is the glue to bring a structure into the
universe of atomized types. You use Positive as if it were Integer because
they participate in a structure of a super-subtype relationship. That does
not make them same type. You cannot force software design into a framework
when types were completely isolated from each other. Types participate in
rich relationships. The language should support declaration and design such
structures of types with static checks. Inventing "profiles", "aspects" etc
gains nothing.

Strong typing is an ability to distinguish types. Not mixing types means
that you could not have subprograms with more than one argument. It is just
crazy. Types are mixed all the time. In a statically typed language all
cases when types get mixed are statically checked. You cannot do that
without taking types apart first.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de