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

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

Le Wed, 08 May 2013 17:29:33 +0200, Dmitry A. Kazakov  
<mailbox@dmitry-kazakov.de> a écrit:
>> I would say there is no general answer without additional informations
>> about what the whole means, and no language or its compiler can tell it  
>> in
>> place of the author (or else, you decide in place of the author, and are
>> back to what it actually is).
>
> First you should be able to define such entities formally = at the  
> language
> level.

Yes, that was the idea. What you say seems equivalent to saying “the  
language should allow to express it”. Actually, it's built‑in only (and so  
also frozen). By the way, old prover software had a comparable issue in  
the paste, they came with built‑in methods to validate this or that kind  
of specific inferences technique within this or that kind of specific  
domain. Then later came provers with a tiny core engine, on which is  
concentrated all the efforts for correctness. The former were more error  
prone (one was even well known as buggy and not soun) and less expressive.  
The latter present their own issues, but are more safe and more  
expressive, as they allow the user to freely express something above, as  
the core ensure the soundness of the inferences (you can get it wrong too,  
but that's not the topic). I don't try to say a general purpose  
programming language should compare to this, just that the way to go ahead  
may be a bit similar: less built‑ins, and more support for soundness (I  
like to say, the value of a language is not in its libraries, this is a  
bit similar here).

>> A basic idea (more easy to say than to do): reuse things like
>> pre/post/pragma‑assert, but whose purpose is to be statically checked  
>> (if
>> it's too complicated to be checked,
>
> Checks if come in question, then only much later after you have  
> formalized
> it.

Static checking is not like dynamic checking. Dynamic checking is just  
checking, while static checking really ensure some assertions. There are  
multiple way to formalize, but sooner or later, all have to arrive at the  
point of providing assertions, or else, you can't derive anything from it.  
So I believe static check one of the way to the formalization.

>> Also to digress but still in some way related, more control on what can  
>> be
>> done of an instance of a type, toward restricting, permitting to deny  
>> the
>> use of some part of an interface,
>
> Each time you do something with a type you get another one.

Yes

> Otherwise it
> becomes untyped. So if you wanted to disallow operations that would make
> another interface.

That's what a subtype is to me (I don't know if it's the proper term; at  
least it seems to match with Ada's own wording).

> To put it differently, there shall be no preconditions
> on types and their operations which aren't trivially true.

I don't understand that point.

> Another question
> is the relationship between the original type and the new one. That  
> brings
> the issue of LSP with it, if you attempt to bring them into one  
> hierarchy.

LSP is a handy principle, the only one practicable with most general  
purpose languages, but that's not the only way to formalize things and  
ensure their correctness; sometime it does not fit. Some relations may be  
preserved, some may not be. If some are preserved, you can count on it,  
while it suffice some are not preserved to make LSP irrelevant, and worst,  
reject the system. That's precisely the case with restricted interfaces,  
it's easy to see some relations are preserved but it does not conform to  
LSP. LSP is nice when applicable, because it is a simple principle; there  
are times where it is too rigid. That's why I focused on the topic of the  
relations and properties individually.

> Ad-hoc supertypes could possibly help.

Yes, that would allow to understand subtypes as any other simply derived  
types. May be the supertype could be automatically or inferred. Or should  
that be always explicit?

> Parallel hierarchies could be an
> alternative.

I will try to imagine what this means or how it works, I don't have a  
clear picture in mind right at the moment.


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