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

["Randy Brukardt" <randy@rrsoftware.com>]

"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. Typing is too rigid to do a good job -- you need to include 
statically known information about the contents of variables and parameters, 
which can change from line-to-line in a program.

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.

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

Yes, of course. You have completely bought the OOP bill of goods that claims 
there is something magical about types.

> Strong typing is madness only without type hierarchies.

Who said anything about getting rid of hierarchies? I think they're greatly 
overused (the number of abstractions that benefit from a hierarchy is quite 
low), but there certainly are cases where they help.

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

> 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. 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". You are already far out 
of the mainstream when you say that. And of course, to allow such a 
difference, you have to go beyond typing, to say "profiles".)

Types form the bedrock of a programming language design, and as such they 
should be unchanging. There should be no difference in typing between 
contexts -- it has to be the same everywhere. To get further checks, you 
have to add on another layer on top.

> 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. And then have lots 
of interconvertability rules. I think you'd quickly reach a level of 
insanity.

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

> 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. And that way can only 
lead to madness.

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

I have no idea what the heck you are talking about now. In any case, it 
makes no sense for me to respond to someone that has an advanced case of 
OOP-fever. Certainly, *one* of us is insane -- time will prove which. No 
point in my spending any more time on this topic unless someone else wants 
to discuss it.

                                     Randy.