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

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

On Thu, 9 May 2013 17:19:14 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:12gn9wvv1gwfk.10ikfju4rzmnj.dlg@40tude.net...
>> 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?
> 
> Yes, because we need to move beyond typing to other forms of static error 
> detection.

Based on what? On individual values?

> Typing is too rigid to do a good job

Typing is necessarily rigid because it is on the next, higher level of
power. Types describe the behavior of sets of values. Nothing you can do
with individual values could come even close to that, except for trivial
cases like enumeration types. And there is the next level, classes describe
behavior of sets of types. And higher levels may probably come.

> I want checking that is *stronger* than what can be provided by statically 
> applied types. Trying to get it by extending the type model directly is 
> madness, especially as it makes sharing much less possible.

No, you will lose a whole universe of checks without gaining anything
useful. Checks of individual values have limits imposed by computability.
Furthermore, focusing on values, you will kill software engineering. Reuse
is what is really important. Checks are only a tool to make reuse safer.

>> 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.
> 
> Yes, of course. You have completely bought the OOP bill of goods that claims 
> there is something magical about types.

Types were known long before OO and first programming languages (Russell,
Church etc).

>> Types are not isolated.
> 
> Again, no one said anything about them being isolated. Although I do think 
> that vast majority of types ought to be separate from other types -- the 
> interactions being handled in the operations, not in the types themselves.

If you want them separate don't blame them for being separate. It was your
choice.

>> 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.
> 
> Great, context-dependent types.

Not at all. It is substitutability which is context-depended and thus must
be formalized as context-independent type relationships (e.g. interfaces).
Existence of negative inverse is no property of Positive. There is no
context where it is. But it is a property of Integer. The context where you
want to have a negative inverse is a context where Positive is not
substitutable for Integer.

[ Since this property is directly observable as the operation "-", there is
no design where Positive could statically be same type as Integer. ]

> There are only two good descriptions for 
> that: "madness", or better, "weak typing". :-) (And of course, there are no 
> contexts where Integer and Positive are "different".

They are different in ALL contexts! Positive (a set of values with
properties of) is not Integer.

> You are already far out 
> of the mainstream when you say that.

Not at all. It is plain school mathematics. Everybody knows that -1 is not
positive.

>> This difference makes them distinct types,
>> nothing else. Where is a difference there is a new type.
> 
> I strongly disagree with this. The only way this could work is for *every* 
> use of *every* entity of a program to be a separate type.

This is how you see it. This is a natural consequence of rejecting types
and thinking in terms of individual values. In this crazy world each value
has a type of its own, which renders types completely useless. Welcome to
OOA/D. (It is funny that you are accusing me of having bought OO's snake
oil (:-))

>> 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.
> 
> Seems to me that you are drunk on the OOP-koolaid. What you can usefully do 
> with type algebra is very limited, and I think we need to go beyond that.
> 
> In particular, I think the Ada model of few types (essentially, initial 
> declaration equivalent) is the way to go; all of the action should be on 
> enhancing subtypes and subprograms such that static checks are possible (by 
> combining constraints, null exclusions, predicates, parameter/result 
> profiles, and possibly other things into an integrated concept).

Concept of what? You are not yet ready with types and want to introduce
something of unknown nature? How these new things will interact each other,
values, types, classes, packages. What is there to check if the properties
of are nowhere stated, meaning is undefined?

>> 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.
> 
> Certainly when you invent ideas like this, which have nothing to do with 
> anything that I said or was thinking about. Obviously, operations of one 
> type need parameters of another type. But your OOP-fever means that you 
> think that this somehow implies the types are related.

What else a relationship is? Types deal with values and operations. There
is nothing else. Since values are not shared (Ada is typed so far), the
only thing which may bind two types is a shared operation.

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