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:1oy5rmprgawqs.1jz36okze0xju$.dlg@40tude.net...
> 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?

What I was calling profiles; Nicolas has provided a reference that says its 
known as "typestate" analysis. It sits on top of types providing more 
information for static checking.


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

I'm adding on top of types, not in place of them. And I don't see what would 
change about software engineering -- that's about visibility control (i.e. 
packages) and strong checking. OOP-madness (inheritance and the like) adds 
little to the ability for reuse -- in large part because it's almost never 
appropriate. (The fact that inheritance is only additive kills most reuse --  
a different abstraction is, for the lack of a better term, different -- it's 
not going to share all or even a lot of the operations.)

...
> Not at all. It is substitutability which is context-depended ...

Bow down to the great god of "substitutability". The real crux of 
OOP-madness -- this is fantasy that does not exist in real problems.


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

Yes, because I'm starting over. That means a nearly clean slate. I want to 
clean up all of those interactions (which are currently a mess), and that 
means rethinking everything. There's no point to small tweaks to Ada (if you 
want model changes), you simply can't get there. You'll just end up adding 
more "gazebos", as you once put it.


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

I don't think operations have anything to do with types: they *use* types, 
they aren't part of them in any way. The "profile" of objects determines 
what operations can be used with them.

Keep in mind that what I've trying to do here is to get the sort of 
statically checked preconditions that you keep saying are necessary. That 
requires formalizing at least part of the state of objects, because a model 
that can't statically check whether files are open in I/O is a pretty 
useless model.

You may describe this is terms of a different formalism, but as far as I'm 
concerned, that's simply trying to confuse the issue. It's confusing enough 
without that kind of "help".

                                       Randy.