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

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt <randy@rrsoftware.com>  
a écrit:

> "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 feel the same. I often though typing can't do everything if it comes  
with value type checking, while in some occasions, I tried to express each  
validity condition with types and then type checking (that ends to be  
crazy, indeed). A simple example, is paired invocation, where whenever a  
sub‑program is is invoked, sooner or later, another sub‑program must be  
invoked too on the same argument, ex. like `Open` and later `Close`. This  
cannot be expressed with types and indeed requires assertions.

But saying “weak” may be erroneously interpreted, and then, the type is  
still the first place to holds the validity rules. In the example above,  
the paired invocation requirement, could be expressed in the type owning  
these two primitives (there is no way to do it actually, except with  
external checking tools and custom rules for this tool). That's just that  
showing the type is used according to the rules it defines, could not be  
ensured with classic type checking (there is no type checking to apply  
here), it would needs assertions in the sources.

In summary I would say: the type is the source of validity rules, but  
can't help to check it, so there is a need for something along to types.  
At least, it would have to go beyond values (so far, types just describe  
values).


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University