* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-09 22:19 ` Randy Brukardt
@ 2013-05-10 3:29 ` Yannick Duchêne (Hibou57)
2013-05-10 4:16 ` Yannick Duchêne (Hibou57)
` (2 more replies)
2013-05-10 3:47 ` Yannick Duchêne (Hibou57)
` (4 subsequent siblings)
5 siblings, 3 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-10 3:29 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-10 3:29 ` Yannick Duchêne (Hibou57)
@ 2013-05-10 4:16 ` Yannick Duchêne (Hibou57)
2013-05-10 8:42 ` Dmitry A. Kazakov
2013-05-10 18:04 ` Niklas Holsti
2 siblings, 0 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-10 4:16 UTC (permalink / raw)
Le Fri, 10 May 2013 05:29:53 +0200, Yannick Duchêne (Hibou57)
<yannick_duchene@yahoo.fr> a écrit:
> […] 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 […]
No, what I said on this is wrong, due to lack of precision. This have to
be an assertion on the outer level, the state of the enclosing scope of
the operations (an implicit value which cannot be explicitly referred to
as a whole with Ada).
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-10 3:29 ` Yannick Duchêne (Hibou57)
2013-05-10 4:16 ` Yannick Duchêne (Hibou57)
@ 2013-05-10 8:42 ` Dmitry A. Kazakov
2013-05-10 11:18 ` Yannick Duchêne (Hibou57)
2013-05-10 18:04 ` Niklas Holsti
2 siblings, 1 reply; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-10 8:42 UTC (permalink / raw)
On Fri, 10 May 2013 05:29:53 +0200, Yannick Duch�ne (Hibou57) wrote:
> I tried to express each validity condition with types and then type checking.
You cannot express program semantics in terms of types.
If you could express semantics, you won't need to program it.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-10 8:42 ` Dmitry A. Kazakov
@ 2013-05-10 11:18 ` Yannick Duchêne (Hibou57)
2013-05-10 12:15 ` Dmitry A. Kazakov
0 siblings, 1 reply; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-10 11:18 UTC (permalink / raw)
Le Fri, 10 May 2013 10:42:25 +0200, Dmitry A. Kazakov
<mailbox@dmitry-kazakov.de> a écrit:
> On Fri, 10 May 2013 05:29:53 +0200, Yannick Duchêne (Hibou57) wrote:
>
>> I tried to express each validity condition with types and then type
>> checking.
>
> You cannot express program semantics in terms of types.
>
> If you could express semantics, you won't need to program it.
I don't understand what means “if you could express semantics, you won't
need to program it”. Or may be you meant the program is already in the
described semantic? If so, that's indeed be true, as the program can then
be derived, but there is not a single possible derivation, there are
typically multiple solutions, so the program still requires human
intervention to be generated.
Then if you see a types as set of axioms, and an instance of a type, as
something with which the axioms are all turned into true hypothesis (you
always need to prove hypothesis are true, before you can infer anything
which in turn is true, and that must be at the object level for program),
then you express semantic with types. And types in Ada, already holds
axioms. Its axiom language is just too limited (ranges and available
operations, that's near to all what's available).
Then again, semantic is expressed with axioms, or else that's not formal
semantic, and that's, say, natural language semantic, always subject to
possible subjective re‑interpretation (no deterministic interpretation).
I will be back to it later and I'm not versed in it enough so far, but
quickly, Isabelle/HOL (HOL stands for Higher Order Logic here), you have
something close to that. With Isabelle, axioms and theorems may be
organized into classes or local theories, which are kind of generic which
are to be instantiated, this instantiation being named “an interpretation
of a local theory”. You instantiate providing functions and values as
arguments.
With this kind of formal system, you typically go from a specification and
derives a program. Ada do it the other way, and go from the program and
prove it matches a specification later (either formally proving with SPARK
or using runtime‑check), or immediately for what is statically checked
(whether or not an operation exist, whether or not a value belongs to the
values of a type). But the concept does not imply a direction and would
make as much sense with the Ada way to go from program and later prove or
check its properties: in both case, you have to express what is to be
verified, whatever you do it before you generate a program or after a
program was authored.
If types could go beyond specification of a simple list of values (and we
already have a taste of that with discriminated records since always and
invariant predicates since Ada 2012) and available sub–programs, you won't
see types as you see it actually, it would look more expressive (and as a
consequence, safer) and less “rigid”.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-10 11:18 ` Yannick Duchêne (Hibou57)
@ 2013-05-10 12:15 ` Dmitry A. Kazakov
2013-05-10 12:40 ` Yannick Duchêne (Hibou57)
0 siblings, 1 reply; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-10 12:15 UTC (permalink / raw)
On Fri, 10 May 2013 13:18:12 +0200, Yannick Duchêne (Hibou57) wrote:
> Le Fri, 10 May 2013 10:42:25 +0200, Dmitry A. Kazakov
> <mailbox@dmitry-kazakov.de> a écrit:
>
>> On Fri, 10 May 2013 05:29:53 +0200, Yannick Duchêne (Hibou57) wrote:
>>
>>> I tried to express each validity condition with types and then type
>>> checking.
>>
>> You cannot express program semantics in terms of types.
>>
>> If you could express semantics, you won't need to program it.
>
> I don't understand what means “if you could express semantics, you won't
> need to program it”. Or may be you meant the program is already in the
> described semantic?
Program implements semantics. If you define the semantics using some other
formalism you don't need the program anymore. The problem is that there is
no formalism, or else the formalism is too powerful for being computable.
> If so, that's indeed be true, as the program can then
> be derived, but there is not a single possible derivation, there are
> typically multiple solutions, so the program still requires human
> intervention to be generated.
Human intervention is needed to handle the semantics, not because of
multiplicity of implementations. You could choose them randomly.
> Then if you see a types as set of axioms, and an instance of a type, as
> something with which the axioms are all turned into true hypothesis (you
> always need to prove hypothesis are true, before you can infer anything
> which in turn is true, and that must be at the object level for program),
> then you express semantic with types. And types in Ada, already holds
> axioms. Its axiom language is just too limited (ranges and available
> operations, that's near to all what's available).
It is not axioms. However the axiomatic framework looks somewhat similar in
the sense that rules of logical inference could be compared with the types
algebra. But there is a sufficient difference that applying algebraic
operations in programming is imperative. You never present a ready type in
order to prove it being a result of some algebraic operations (=algebraic
type). Maybe only in academic studies. Rather you apply operations directly
and the result becomes algebraic merely per construction.
> Then again, semantic is expressed with axioms, or else that's not formal
> semantic, and that's, say, natural language semantic, always subject to
> possible subjective re‑interpretation (no deterministic interpretation).
No, the program semantics is the meaning of what the program does (to the
customer). That lies outside the language. Not to confuse with the language
semantics which describes how to execute the code (to the CPU).
> I will be back to it later and I'm not versed in it enough so far, but
> quickly, Isabelle/HOL (HOL stands for Higher Order Logic here), you have
> something close to that. With Isabelle, axioms and theorems may be
> organized into classes or local theories, which are kind of generic which
> are to be instantiated, this instantiation being named “an interpretation
> of a local theory”. You instantiate providing functions and values as
> arguments.
I am not familiar with that, but formal methods are always a meta language
relatively to the programming language and its type system, which are the
object language for them. You never mix the two.
> With this kind of formal system, you typically go from a specification and
> derives a program.
That won't work. If you can derive the program (in the object language) you
don't need the object language anymore. If that indeed works, as it does
with the Assembly language, you move up to the meta language (higher-level
programming language in this case) and forget about silly lower-level
stuff. Regarding specification languages and modeling language I have
serious reservations about them being capable to replace Ada and other
general purpose languages.
> If types could go beyond specification of a simple list of values (and we
> already have a taste of that with discriminated records since always and
> invariant predicates since Ada 2012) and available sub–programs, you won't
> see types as you see it actually, it would look more expressive (and as a
> consequence, safer) and less “rigid”.
I don't see how Ada 2012 makes it more expressive. It did not extend types
algebra in any significant way.
BTW, static checks if have something to do with expressiveness, then by
hampering it. Because it is evident that the more powerful constructs you
have, less you could prove about their outcome. The most notorious example
is goto. The art of language design is to deploy least powerful constructs,
while keeping it useful for programming.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-10 12:15 ` Dmitry A. Kazakov
@ 2013-05-10 12:40 ` Yannick Duchêne (Hibou57)
2013-05-10 12:59 ` Yannick Duchêne (Hibou57)
2013-05-10 13:54 ` Dmitry A. Kazakov
0 siblings, 2 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-10 12:40 UTC (permalink / raw)
Le Fri, 10 May 2013 14:15:35 +0200, Dmitry A. Kazakov
<mailbox@dmitry-kazakov.de> a écrit:
>> If so, that's indeed be true, as the program can then
>> be derived, but there is not a single possible derivation, there are
>> typically multiple solutions, so the program still requires human
>> intervention to be generated.
>
> Human intervention is needed to handle the semantics, not because of
> multiplicity of implementations. You could choose them randomly.
You can't choose randomly, the program must have runtime properties as
well.
Another case, is with what in the domain is known as shallow embedding;
this means you model the target language (or a subset of it or some
constructs of it) in the terms of the formal language, then write the
program in the target language indirectly writing proof involving these
constructs (I mean, the ones representing the target language). Then, you
ends with a program in the target language with syntactic transformations.
There is another way to do, which is named deep embedding, but I don't
really know it and don't like it anyway.
In all cases (either one of the three), the target language is always
there, it just appears at different stage, sometime immediately from the
start, sometime only at the final stage.
>> With this kind of formal system, you typically go from a specification
>> and
>> derives a program.
>
> That won't work. If you can derive the program (in the object language)
> you don't need the object language anymore.
You really can't say “it won't work”, since there are people who already
do this, and that works, and that's not restricted to “academic
experiments”. The object language is still needed, as further more, Ada
had even been famously involved as a target language with the B formal
method (whose target languages may be either Ada or C). I know it was used
in france for the software of some subway lines in Paris (they used B and
Ada 95 if I'm not wrong). This was from specification to Ada, and not from
Ada to proof (as SPARK do).
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-10 12:40 ` Yannick Duchêne (Hibou57)
@ 2013-05-10 12:59 ` Yannick Duchêne (Hibou57)
2013-05-10 13:54 ` Dmitry A. Kazakov
1 sibling, 0 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-10 12:59 UTC (permalink / raw)
Le Fri, 10 May 2013 14:40:00 +0200, Yannick Duchêne (Hibou57)
<yannick_duchene@yahoo.fr> a écrit:
> Le Fri, 10 May 2013 14:15:35 +0200, Dmitry A. Kazakov
> <mailbox@dmitry-kazakov.de> a écrit:
>>> If so, that's indeed be true, as the program can then
>>> be derived, but there is not a single possible derivation, there are
>>> typically multiple solutions, so the program still requires human
>>> intervention to be generated.
>>
>> Human intervention is needed to handle the semantics, not because of
>> multiplicity of implementations. You could choose them randomly.
>
> You can't choose randomly, the program must have runtime properties as
> well.
I should have given another example, a more obvious one: as the program
derivation is a consequence of a proof the specification is satisfiable
(the proof and the program are the same thing), automated program
generation from the specification, would implies automated proof. This
does not exist with the actual technology, if not for trivial stuffs. So
far you have proof assistants, not automated provers (just some steps of
proofs may be automated, if the user request some help from the assistant…
but it may fail and it's not usable for program generation as far as I
know).
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-10 12:40 ` Yannick Duchêne (Hibou57)
2013-05-10 12:59 ` Yannick Duchêne (Hibou57)
@ 2013-05-10 13:54 ` Dmitry A. Kazakov
2013-05-10 14:01 ` Yannick Duchêne (Hibou57)
1 sibling, 1 reply; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-10 13:54 UTC (permalink / raw)
On Fri, 10 May 2013 14:40:00 +0200, Yannick Duchêne (Hibou57) wrote:
> Le Fri, 10 May 2013 14:15:35 +0200, Dmitry A. Kazakov
> <mailbox@dmitry-kazakov.de> a écrit:
>>> If so, that's indeed be true, as the program can then
>>> be derived, but there is not a single possible derivation, there are
>>> typically multiple solutions, so the program still requires human
>>> intervention to be generated.
>>
>> Human intervention is needed to handle the semantics, not because of
>> multiplicity of implementations. You could choose them randomly.
>
> You can't choose randomly, the program must have runtime properties as
> well.
The only properties a program must have are derived from its semantics, per
definition.
>>> With this kind of formal system, you typically go from a specification
>>> and derives a program.
>>
>> That won't work. If you can derive the program (in the object language)
>> you don't need the object language anymore.
>
> You really can't say “it won't work”, since there are people who already
> do this,
That is their problem. People do crazy things all the time.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-10 13:54 ` Dmitry A. Kazakov
@ 2013-05-10 14:01 ` Yannick Duchêne (Hibou57)
2013-05-10 14:27 ` Dmitry A. Kazakov
0 siblings, 1 reply; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-10 14:01 UTC (permalink / raw)
Le Fri, 10 May 2013 15:54:40 +0200, Dmitry A. Kazakov
<mailbox@dmitry-kazakov.de> a écrit:
>>> Human intervention is needed to handle the semantics, not because of
>>> multiplicity of implementations. You could choose them randomly.
>>
>> You can't choose randomly, the program must have runtime properties as
>> well.
>
> The only properties a program must have are derived from its semantics,
> per definition.
The time required for a computation, the memory used, are not part of the
semantic. Computational complexity is not semantic.
>>> That won't work. If you can derive the program (in the object language)
>>> you don't need the object language anymore.
>>
>> You really can't say “it won't work”, since there are people who already
>> do this,
>
> That is their problem. People do crazy things all the time.
What's crazy with this?
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-10 14:01 ` Yannick Duchêne (Hibou57)
@ 2013-05-10 14:27 ` Dmitry A. Kazakov
2013-05-10 15:20 ` Yannick Duchêne (Hibou57)
2013-05-11 7:22 ` Georg Bauhaus
0 siblings, 2 replies; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-10 14:27 UTC (permalink / raw)
On Fri, 10 May 2013 16:01:46 +0200, Yannick Duchêne (Hibou57) wrote:
> Le Fri, 10 May 2013 15:54:40 +0200, Dmitry A. Kazakov
> <mailbox@dmitry-kazakov.de> a écrit:
>>>> Human intervention is needed to handle the semantics, not because of
>>>> multiplicity of implementations. You could choose them randomly.
>>>
>>> You can't choose randomly, the program must have runtime properties as
>>> well.
>>
>> The only properties a program must have are derived from its semantics,
>> per definition.
>
> The time required for a computation, the memory used, are not part of the
> semantic.
It is for RT or else irrelevant.
> Computational complexity is not semantic.
And so irrelevant.
>>>> That won't work. If you can derive the program (in the object language)
>>>> you don't need the object language anymore.
>>>
>>> You really can't say “it won't work”, since there are people who already
>>> do this,
>>
>> That is their problem. People do crazy things all the time.
>
> What's crazy with this?
Because it is impossible to do. When meant seriously beyond academic
exercises, it is most likely undecidable, incomputable, halting etc.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-10 14:27 ` Dmitry A. Kazakov
@ 2013-05-10 15:20 ` Yannick Duchêne (Hibou57)
2013-05-11 7:22 ` Georg Bauhaus
1 sibling, 0 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-10 15:20 UTC (permalink / raw)
Le Fri, 10 May 2013 16:27:42 +0200, Dmitry A. Kazakov
<mailbox@dmitry-kazakov.de> a écrit:
>> The time required for a computation, the memory used, are not part of
>> the
>> semantic.
>
> It is for RT or else irrelevant.
>
>> Computational complexity is not semantic.
>
> And so irrelevant.
I've never asserted semantic is everything (and even suggested the
opposite). Runtime properties is another aspect. Not the same methods, not
the same formalisms, these are orthogonal aspects (or more or less).
> Because it is impossible to do. When meant seriously beyond academic
> exercises, it is most likely undecidable, incomputable, halting etc.
That's not impossible nor academic only, that's used for real life case (I
gave an example, there are many others). Generating program from
specification does not prevent nor disallow proofs of bounded runtime
requirement.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-10 14:27 ` Dmitry A. Kazakov
2013-05-10 15:20 ` Yannick Duchêne (Hibou57)
@ 2013-05-11 7:22 ` Georg Bauhaus
1 sibling, 0 replies; 202+ messages in thread
From: Georg Bauhaus @ 2013-05-11 7:22 UTC (permalink / raw)
On 10.05.13 16:27, Dmitry A. Kazakov wrote:
> On Fri, 10 May 2013 16:01:46 +0200, Yannick Duchêne (Hibou57) wrote:
>
>> Le Fri, 10 May 2013 15:54:40 +0200, Dmitry A. Kazakov
>> <mailbox@dmitry-kazakov.de> a écrit:
>>>>> Human intervention is needed to handle the semantics, not because of
>>>>> multiplicity of implementations. You could choose them randomly.
>>>>
>>>> You can't choose randomly, the program must have runtime properties as
>>>> well.
>>>
>>> The only properties a program must have are derived from its semantics,
>>> per definition.
>>
>> The time required for a computation, the memory used, are not part of the
>> semantic.
>
> It is for RT or else irrelevant.
"It" becomes a compile time thing as soon as we can state meaningfully
(hence, checked by the compiler), in source text, that some part of a
program must (and will) make bounded use of resources, where "bounded"
is not trivially true but specifically true of the program being
translated.
Semi-formally, the data structure parts of C++ and Ada have made a
move in this direction by advising that certain language-provided
operations on containers be bounded specifically.
It will be sufficient if compilers decide this when translating the
very few (compared to the possible) of the non-undecidable programs
that warrant our profession.
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-10 3:29 ` Yannick Duchêne (Hibou57)
2013-05-10 4:16 ` Yannick Duchêne (Hibou57)
2013-05-10 8:42 ` Dmitry A. Kazakov
@ 2013-05-10 18:04 ` Niklas Holsti
2013-05-10 19:33 ` Yannick Duchêne (Hibou57)
2013-05-11 0:18 ` Randy Brukardt
2 siblings, 2 replies; 202+ messages in thread
From: Niklas Holsti @ 2013-05-10 18:04 UTC (permalink / raw)
On 13-05-10 06:29 , Yannick Duchêne (Hibou57) wrote:
> Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt
...
>> 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.
Are you familiar with the "typestate" concept? As I understand it, the
intent is to check state-sequence rules such as Open-followed-by-Close.
See http://en.wikipedia.org/wiki/Typestate_analysis.
--
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
. @ .
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-10 18:04 ` Niklas Holsti
@ 2013-05-10 19:33 ` Yannick Duchêne (Hibou57)
2013-05-11 0:18 ` Randy Brukardt
1 sibling, 0 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-10 19:33 UTC (permalink / raw)
Le Fri, 10 May 2013 20:04:42 +0200, Niklas Holsti
<niklas.holsti@tidorum.invalid> a écrit:
> Are you familiar with the "typestate" concept? As I understand it, the
> intent is to check state-sequence rules such as Open-followed-by-Close.
> See http://en.wikipedia.org/wiki/Typestate_analysis.
I did not knew it before. Thanks for the pointer, that's always good to
know the name of things (may be interesting to see if it's related to
temporal logic).
Just for the anecdote, the way I tried to solve it with static check, was
using typed tokens, returned and/or required by operations. Say an
operation B is allowed to occur only if an operation A occurred before.
The operation A returns a value of type TA. As B requires to occurs only
after A, then it can requires a token of type TA as its input arguments.
Similarly, B may return a token of type TB, which may be required by any
operation which must occur only after B.
To be trustable, it requires TA, TB and so on, cannot be created out of
control of A, B an so on, so it must be limited types with unknown
discriminant (the latter to force initialization).
Well, that looks a nice hack, it's statically checked, but that's limited
and bloats everything, and near to be unusable due to the required
initialisation (imagine writing a program all in the declarative part).
Then, no way to tell B must always occur later after A if ever A occurred.
It also only know about simple sequence, and can't differentiate between
A;B;C and A;C. It can't differentiate neither between instances (there is
no way to check a token was return by an operation on this or that
instance). So finally, I gave up with this hack.
That's what I was thinking about, when I said it can indeed become crazy
to try to express all validity rules using the type system.
There is another less restrictive way to do, except it cannot statically
check, which ends to be the same as pre/post, and that's finally better to
just use pre/post in this case (at that time, Ada 2012 was not there).
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-10 18:04 ` Niklas Holsti
2013-05-10 19:33 ` Yannick Duchêne (Hibou57)
@ 2013-05-11 0:18 ` Randy Brukardt
2013-05-11 7:14 ` Yannick Duchêne (Hibou57)
2013-05-11 21:06 ` Niklas Holsti
1 sibling, 2 replies; 202+ messages in thread
From: Randy Brukardt @ 2013-05-11 0:18 UTC (permalink / raw)
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1673 bytes --]
"Niklas Holsti" <niklas.holsti@tidorum.invalid> wrote in message
news:av4r5qFitfiU1@mid.individual.net...
> On 13-05-10 06:29 , Yannick Duch�ne (Hibou57) wrote:
>> Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt
> ...
>>> 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.
>
> Are you familiar with the "typestate" concept? As I understand it, the
> intent is to check state-sequence rules such as Open-followed-by-Close.
> See http://en.wikipedia.org/wiki/Typestate_analysis.
Thanks for the reference. I doubted that the idea was new (there are no new
ideas), but I hadn't heard of it before. I don't like the name much, because
it feeds into the "type is everything" madness that Dmitry exhibits so
clearly. This clearly (just like constraints and predicates) is something
that's added in addition to type analysis; it's not part of it at all.
Randy.
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 0:18 ` Randy Brukardt
@ 2013-05-11 7:14 ` Yannick Duchêne (Hibou57)
2013-05-11 21:06 ` Niklas Holsti
1 sibling, 0 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-11 7:14 UTC (permalink / raw)
Le Sat, 11 May 2013 02:18:30 +0200, Randy Brukardt <randy@rrsoftware.com>
a écrit:
> Thanks for the reference. I doubted that the idea was new (there are no
> new
> ideas), but I hadn't heard of it before. I don't like the name much,
> because
> it feeds into the "type is everything" madness that Dmitry exhibits so
> clearly. This clearly (just like constraints and predicates) is something
> that's added in addition to type analysis; it's not part of it at all.
I agree this cannot be checked with typing and needs an additional
analysis, that seems obvious. But where would you state the predicates to
be verified, if not in something which is bounded to the type? The type
definition it self or its methods, is the only one place where to requires
the predicates to be verified; this can't move around freely, this have to
be bound to it in some way.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 0:18 ` Randy Brukardt
2013-05-11 7:14 ` Yannick Duchêne (Hibou57)
@ 2013-05-11 21:06 ` Niklas Holsti
2013-05-11 23:19 ` Shark8
2013-05-12 6:44 ` Yannick Duchêne (Hibou57)
1 sibling, 2 replies; 202+ messages in thread
From: Niklas Holsti @ 2013-05-11 21:06 UTC (permalink / raw)
On 13-05-11 03:18 , Randy Brukardt wrote:
> "Niklas Holsti" <niklas.holsti@tidorum.invalid> wrote in message
> news:av4r5qFitfiU1@mid.individual.net...
>> On 13-05-10 06:29 , Yannick Duch�ne (Hibou57) wrote:
>>> Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt
>> ...
>>>> 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.
>>
>> Are you familiar with the "typestate" concept? As I understand it, the
>> intent is to check state-sequence rules such as Open-followed-by-Close.
>> See http://en.wikipedia.org/wiki/Typestate_analysis.
>
> Thanks for the reference. I doubted that the idea was new (there are no new
> ideas), but I hadn't heard of it before.
I'm not sure if "typestate" matches all of what you were describing or
thinking of -- I meant it only as a pointer to Yannick for things like
the Open-Close protocol example. But if it resonates with your thinking,
good.
> I don't like the name much, because
> it feeds into the "type is everything" madness that Dmitry exhibits so
> clearly. This clearly (just like constraints and predicates) is something
> that's added in addition to type analysis; it's not part of it at all.
I haven't studied typestate analysis at all deeply. I had a look at the
"Plaid" language referenced from the Wikipedia article, at
http://www.cs.cmu.edu/~aldrich/plaid/, and was a bit surprised to
understand that Ada subtypes come rather close to it, in particular
subtypes of discriminated record types with variants. The value of the
discriminant represents the state, with certain components of the record
(= attributes of the object or type) existing or not existing depending
on the variant selected by the discriminant.
For the Open-Close example:
type File_State is (Is_Closed, Is_Open);
type File_Object (State : File_State := Is_Closed) is
record
case State is
when Is_Closed => null;
when Is_Open => Handle : System.IO.File_Handle;
end case;
end record;
subtype Closed_File is File_Object (State => Is_Closed);
subtype Open_File is File_Object (State => Is_Open );
By using subtypes on formal parameters, we can indicate that the
available operations on a File_Object depend on the actual subtype
(i.e. the state), except for one deficiency, on which more below.
First, reading and writing is possible only for open files:
procedure Read (File : in Open_File; ...)
procedure Write (File : in Open_File; ...)
Second, a Closed file can be Opened, and an Open file can be Closed:
procedure Open (File : in out Closed_File);
procedure Close (File : in out Open_File );
The problem here is that these operations should change the subtype of
the "in out" parameter: Open changes the File from Closed_File to
Open_File, and Close changes it from Open_File to Closed_File. However,
Ada does not let us specify such changes, in the subprogram profile.
(This can of course be specified with pre- and post-conditions, but I'm
looking for a closer connection between the subprogram profile and the
subtypes.)
Well, why is Ada limited in this way? There is no real reason why an "in
out" parameter should have the same constraints on input and on output.
So let us extend Ada to allow different "in" and "out" subtypes:
-- Extended Ada:
procedure Open (File : in Closed_File out Open_File ; ...);
procedure Close (File : in Open_File out Closed_File; ...);
This gives us exactly the open/close typestate example. A compiler with
strong value-range analysis should then be able to deduce, for example,
that the "in" constraint check on a particular call of Open, Close,
Read, or Write always succeeds (= typestate correctness) or may or must
fail (various degrees of typestate incorrectness). I believe that many
current compilers could do such value-range analysis, and thus Ada could
support this kind of typestate concept with rather small language changes.
(You may ask: if an "in out" parameter has different "in" and "out"
subtypes, what subtype is applied when the formal parameter is used or
assigned within the subprogram body? I think the logical answer would be
the "disjunctive subtype" that represents the union of the "in" and
"out" subtypes, which unfortunately could be a subtype with "holes". But
I think that would be manageable, since this disjunctive subtype would
have at most two separate components, i.e. at most one hole.)
--
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
. @ .
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 21:06 ` Niklas Holsti
@ 2013-05-11 23:19 ` Shark8
2013-05-12 6:09 ` Niklas Holsti
2013-05-12 6:44 ` Yannick Duchêne (Hibou57)
1 sibling, 1 reply; 202+ messages in thread
From: Shark8 @ 2013-05-11 23:19 UTC (permalink / raw)
On Saturday, May 11, 2013 3:06:25 PM UTC-6, Niklas Holsti wrote:
>
> Well, why is Ada limited in this way? There is no real reason why an "in
> out" parameter should have the same constraints on input and on output.
What? Ada's not constrained like that, at least as you're implying:
Given the types you have:
>
> type File_State is (Is_Closed, Is_Open);
>
> type File_Object (State : File_State := Is_Closed) is
> record
> case State is
> when Is_Closed => null;
> when Is_Open => Handle : System.IO.File_Handle;
> end case;
> end record;
>
> subtype Closed_File is File_Object (State => Is_Closed);
> subtype Open_File is File_Object (State => Is_Open );
the proper way to formulate _EXACTLY_ what you want is this:
procedure Read (File : in out File_Object; ...)
with pre => File in Closed_File, post => file in Open_File;
Or am I wrong?
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 23:19 ` Shark8
@ 2013-05-12 6:09 ` Niklas Holsti
2013-05-14 2:02 ` Randy Brukardt
0 siblings, 1 reply; 202+ messages in thread
From: Niklas Holsti @ 2013-05-12 6:09 UTC (permalink / raw)
On 13-05-12 02:19 , Shark8 wrote:
> On Saturday, May 11, 2013 3:06:25 PM UTC-6, Niklas Holsti wrote:
>>
>> Well, why is Ada limited in this way? There is no real reason why an "in
>> out" parameter should have the same constraints on input and on output.
>
> What? Ada's not constrained like that, at least as you're implying:
When you declare an "in out" parameter, Ada now requires that you
specify the same subtype for both roles. In the example, if the File
parameter to Open is declared as "in out Closed_File", but Open tries to
change the parameter to (State => Is_Open, Handle => ...) a
Constraint_Error results at run-time.
> Given the types you have:
>>
>> type File_State is (Is_Closed, Is_Open);
>>
>> type File_Object (State : File_State := Is_Closed) is
>> record
>> case State is
>> when Is_Closed => null;
>> when Is_Open => Handle : System.IO.File_Handle;
>> end case;
>> end record;
>>
>> subtype Closed_File is File_Object (State => Is_Closed);
>> subtype Open_File is File_Object (State => Is_Open );
>
> the proper way to formulate _EXACTLY_ what you want is this:
>
> procedure Read (File : in out File_Object; ...)
> with pre => File in Closed_File, post => file in Open_File;
(I think you mean "procedure Open" there, not "Read".)
As I said, it can be expressed with pre- and post-conditions in this
way, but then the parameter profile does not mention the subtypes and
instead uses the unconstrained type (here File_Object). As I also said,
I wanted the subtype changes to be visible in the subprogram profile, to
show more clearly (or at least, more traditionally) how the availability
of the subprogram depends on the state (i.e. the subtype) of the
parameter, and how it affects the state.
To condense my points:
1. The typestate concept, as implemented in the Plaid language, seems
(after my brief study of Plaid) to be implementable in Ada through
discriminated records with variants.
2. The influence of the current typestate of an object, on the set of
subprograms (operations) available for the object, can be represented as
constraints on the "in" subtype of the object, and the typestate changes
can be represented as the "out" subtype. In current Ada, of course, the
subtype checks in principle occur at run-time, so typestate correctness
is not checked at compile-time. Moreover, current Ada does not allow the
formal subtype (as written in the profile) to be different for the "in"
and "out" roles.
3. Those different "in" and "out" constraints can be implemented in Ada
2012 as pre/post-conditions, as you say.
4. A closer match to Plaid can be achieved if Ada is extended to allow
different subtypes for the "in" and "out" roles of an "in out" parameter.
As the pre/post-condition feature of Ada 2012 becomes more familiar,
perhaps the pre- and post-conditions will be seen as a more integrated
part of the subprogram's profile, and there is no reason to consider
changes to the formal subtypes allowed in the language (point 4).
On the other hand, it seems to me that there are other cases, not
perhaps related to typestate, where it would be natural to specify
different "in" and "out" subtypes for an "in out" parameter. Something
as simple as:
procedure Increment (Counter : in out Natural)
could become
-- Extended Ada:
procedure Increment (
Counter : in Natural range 0 .. Natural'Last - 1
out Positive);
Of course, all such different in/out constraints can be expressed using
the "heavy guns" of pre/post-conditions, so perhaps this suggestion is
out of date after Ada 2012. Any compiler powerful enough to do useful
typestate analysis based on the formal parameter subtypes is probably
able to do the same analysis using the corresponding
pre/post-conditions, at least when the conditions take the simple form
"parameter in subtype".
It is interesting that Randy thinks his ideas regarding a future
replacement for Ada resemble the typestate concept, but that the
typestate concept as implemented in Plaid seems to be implementable in
Ada 2012. Perhaps Randy's ideas go much further than this, however.
--
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
. @ .
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-12 6:09 ` Niklas Holsti
@ 2013-05-14 2:02 ` Randy Brukardt
0 siblings, 0 replies; 202+ messages in thread
From: Randy Brukardt @ 2013-05-14 2:02 UTC (permalink / raw)
"Niklas Holsti" <niklas.holsti@tidorum.invalid> wrote in message
news:av8pvtFehv2U1@mid.individual.net...
...
> It is interesting that Randy thinks his ideas regarding a future
> replacement for Ada resemble the typestate concept, but that the
> typestate concept as implemented in Plaid seems to be implementable in
> Ada 2012. Perhaps Randy's ideas go much further than this, however.
The main thing I was thinking about was some extension to the things that
have to be compile-time analyzable (as Static Predicates are in Ada 2012).
Probably the basis of them would remain subtypes and subprogram profiles
(via preconditions and postconditions). For the Open example, that requires
some way to encode the notion of "properties" in a statically understandable
way. Perhaps you are right that discriminants would do the trick, but we'd
want them to be "virtual" discriminants without any runtime cost.
I agree that you can get the effect of typestate analysis in Ada 2012 using
discriminants, predicates, and pre/postconditions, but those would be
checked at runtime. The key here for me is to require static detection of
these errors, even when variables and unconstrained formal parameters are
involved.
Anyway, I'm just musing here as opposed to having fully worked out ideas. So
I could in fact be going down the wrong path.
Randy.
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 21:06 ` Niklas Holsti
2013-05-11 23:19 ` Shark8
@ 2013-05-12 6:44 ` Yannick Duchêne (Hibou57)
2013-05-12 8:10 ` Niklas Holsti
1 sibling, 1 reply; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-12 6:44 UTC (permalink / raw)
Le Sat, 11 May 2013 23:06:25 +0200, Niklas Holsti
<niklas.holsti@tidorum.invalid> a écrit:
> type File_State is (Is_Closed, Is_Open);
>
> type File_Object (State : File_State := Is_Closed) is
> record
> case State is
> when Is_Closed => null;
> when Is_Open => Handle : System.IO.File_Handle;
> end case;
> end record;
>
> subtype Closed_File is File_Object (State => Is_Closed);
> subtype Open_File is File_Object (State => Is_Open );
>
> By using subtypes on formal parameters, we can indicate that the
> available operations on a File_Object depend on the actual subtype
> (i.e. the state), except for one deficiency, on which more below.
>
> First, reading and writing is possible only for open files:
>
> procedure Read (File : in Open_File; ...)
> procedure Write (File : in Open_File; ...)
>
> Second, a Closed file can be Opened, and an Open file can be Closed:
>
> procedure Open (File : in out Closed_File);
> procedure Close (File : in out Open_File );
>
> The problem here is that these operations should change the subtype of
> the "in out" parameter: Open changes the File from Closed_File to
> Open_File, and Close changes it from Open_File to Closed_File.
Additionally to the idea you suggested, that may also suggest to use a
function instead of a procedure with in/out parameter, with a new
declaration for each of the important state changes which would become
clearly visible (still what if this already was a function already
returning something… Ada functions can return only one single element).
There is now the question about compilers: are compilers clever enough to
statically catch subtype miss‑match in such a use cases and give warnings
(I believe no), and are compilers clever enough to optimize out multiple
object declaration into a single one, changing its subtype (I believe no,
too), while the latter is not an issue if you use a default discriminant
as you did.
Another issue with subtype, is that it requires the `File_Object` full
definition to be public, or else, there is no way to define a subtype of
it as the example do (no opaque type).
The idea is still nice and worth to investigate.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-12 6:44 ` Yannick Duchêne (Hibou57)
@ 2013-05-12 8:10 ` Niklas Holsti
2013-05-12 8:49 ` Yannick Duchêne (Hibou57)
2013-05-12 18:56 ` Jeffrey Carter
0 siblings, 2 replies; 202+ messages in thread
From: Niklas Holsti @ 2013-05-12 8:10 UTC (permalink / raw)
On 13-05-12 09:44 , Yannick Duchêne (Hibou57) wrote:
> Le Sat, 11 May 2013 23:06:25 +0200, Niklas Holsti
> <niklas.holsti@tidorum.invalid> a écrit:
>
>> type File_State is (Is_Closed, Is_Open);
>>
>> type File_Object (State : File_State := Is_Closed) is
>> record
>> case State is
>> when Is_Closed => null;
>> when Is_Open => Handle : System.IO.File_Handle;
>> end case;
>> end record;
>>
>> subtype Closed_File is File_Object (State => Is_Closed);
>> subtype Open_File is File_Object (State => Is_Open );
>>
>> By using subtypes on formal parameters, we can indicate that the
>> available operations on a File_Object depend on the actual subtype
>> (i.e. the state), except for one deficiency, on which more below.
>>
>> First, reading and writing is possible only for open files:
>>
>> procedure Read (File : in Open_File; ...)
>> procedure Write (File : in Open_File; ...)
>>
>> Second, a Closed file can be Opened, and an Open file can be Closed:
>>
>> procedure Open (File : in out Closed_File);
>> procedure Close (File : in out Open_File );
>>
>> The problem here is that these operations should change the subtype of
>> the "in out" parameter: Open changes the File from Closed_File to
>> Open_File, and Close changes it from Open_File to Closed_File.
>
> Additionally to the idea you suggested, that may also suggest to use a
> function instead of a procedure with in/out parameter, with a new
> declaration for each of the important state changes which would become
> clearly visible (still what if this already was a function already
> returning something… Ada functions can return only one single element).
You mean like this:
function Open (File : in Closed_File) return Open_File;
function Close (File : in Open_File ) return Closed_File;
I agree that this is a possible approach. This would work, but at the
cost of writing the parameter/object name twice in each call:
File : File_Object;
...
File := Open (File);
File := Close (File);
But this code seems to cause a problem:
File1, File2 : File_Object;
...
File1 := Open (File1);
File2 := Close (File1);
Now File2 is a clone of File1, and the underlying system file is closed,
but File1 still considers it open. (This may of course be acceptable to
the specific underlying system and not lead to an error, but in general
I believe that such side-effects could be problematic.)
The "function" approach thus tends to clone objects, and to lose the
"object identity".
If we want to preserve object identity under that approach, I think we
need a "linear type system"
(http://en.wikipedia.org/wiki/Linear_type_system) in which each variable
can be used exactly once. However, every use (e.g. as a parameter to a
function) can produce a new incarnation of the object (the function
return value), which can be assigned to a new variable, so the object
lives on. However, this would be a BIG change to the language.
> There is now the question about compilers: are compilers clever enough
> to statically catch subtype miss‑match in such a use cases and give
> warnings (I believe no),
I think that if this issue of subtype matching comes to be considered
important, compiler writers could give it more attention, and
conservative (but incomplete) static-analysis solutions could be
implemented with current technology.
> and are compilers clever enough to optimize out
> multiple object declaration into a single one, changing its subtype (I
> believe no, too),
Those problems are solved by a linear type system. But I agree with you
that it is too much to expect that the compiler would automatically
implement an Ada-like program using linear typing behind the scenes.
> Another issue with subtype, is that it requires the `File_Object` full
> definition to be public, or else, there is no way to define a subtype of
> it as the example do (no opaque type).
Yes, that could be a problem. The language might allow the declaration
of subtypes of opaque types, with opaque constraints. That does not seem
too hard to implement if the type and subtypes are fully defined in the
private part of a package, but it seems more difficult if the full type
declaration is deferred (through an access type) to the package body.
--
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
. @ .
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-12 8:10 ` Niklas Holsti
@ 2013-05-12 8:49 ` Yannick Duchêne (Hibou57)
2013-05-12 18:56 ` Jeffrey Carter
1 sibling, 0 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-12 8:49 UTC (permalink / raw)
Le Sun, 12 May 2013 10:10:01 +0200, Niklas Holsti
<niklas.holsti@tidorum.invalid> a écrit:
> You mean like this:
>
> function Open (File : in Closed_File) return Open_File;
> function Close (File : in Open_File ) return Closed_File;
>
> I agree that this is a possible approach. This would work, but at the
> cost of writing the parameter/object name twice in each call:
Yes, that was that. I don't bother about writing more when it that makes
things more readable.
> File : File_Object;
> ...
> File := Open (File);
> File := Close (File);
>
> But this code seems to cause a problem:
>
> File1, File2 : File_Object;
> ...
> File1 := Open (File1);
> File2 := Close (File1);
>
> Now File2 is a clone of File1, and the underlying system file is closed,
> but File1 still considers it open.
Interesting point. Note the the procedural way present the same issue, as
the object may be copied too, even if limited, using component by
component copy (as with actual Ada, the type cannot be private for the
reason given before). Less likely to occurs, but if it can occurs, it's
enough to say the issue is still there.
>
> The "function" approach thus tends to clone objects, and to lose the
> "object identity".
The topic of object identity is interesting, I have not though about it.
That's finally an issue similar to aliasing here… as the file type is
finally a kind of reference, via its handle.
> If we want to preserve object identity under that approach, I think we
> need a "linear type system"
> (http://en.wikipedia.org/wiki/Linear_type_system)
Your nickname must Santa Clause :) Thanks for the new pointer, again.
> Yes, that could be a problem. The language might allow the declaration
> of subtypes of opaque types, with opaque constraints.
But the subtype would not have readable sense if the constraints would be
opaque. Or else as an alternative, may be Ada could allow partly unknown
discriminant (something I miss):
-- Valid actual Ada:
type T1 (<>) is private;
-- Invalid, actual Ada don't permits this:
type T2 (Foo: Foo_Type; <>) is private;
As an unrelated side note, something I miss too with private types, is the
ability for the completion to be a subtype (actual Ada requires it to be a
type‑new or a record).
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-12 8:10 ` Niklas Holsti
2013-05-12 8:49 ` Yannick Duchêne (Hibou57)
@ 2013-05-12 18:56 ` Jeffrey Carter
2013-05-12 22:15 ` Robert A Duff
2013-05-13 5:21 ` Niklas Holsti
1 sibling, 2 replies; 202+ messages in thread
From: Jeffrey Carter @ 2013-05-12 18:56 UTC (permalink / raw)
On 05/12/2013 01:10 AM, Niklas Holsti wrote:
>
> You mean like this:
>
> function Open (File : in Closed_File) return Open_File;
> function Close (File : in Open_File ) return Closed_File;
>
> I agree that this is a possible approach. This would work, but at the
> cost of writing the parameter/object name twice in each call:
>
> File : File_Object;
> ...
> File := Open (File);
> File := Close (File);
I'm not sure I see the point in having an object for a closed file, other than
the requirements of low-level languages in which such things were 1st
implemented. Why not something like
type File_Info (<>) is tagged limited private;
function Open (Name : ...; ...) return File_Info;
function Create (Name : ...; ...) return File_Info;
function Read (File : in out File_Info) return ...;
procedure Write (File : in out File_Info; Item : in ...);
declare
File : File_Info := Open ("junk", ...);
begin
Data := Read (File);
...
end;
A File_Info must be opened or created when declared, and is closed when it's
finalized.
--
Jeff Carter
"C++ is like giving an AK-47 to a monk, shooting him
full of crack and letting him loose in a mall and
expecting him to balance your checking account
'when he has the time.'"
Drew Olbrich
52
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-12 18:56 ` Jeffrey Carter
@ 2013-05-12 22:15 ` Robert A Duff
2013-05-13 0:26 ` Jeffrey Carter
` (2 more replies)
2013-05-13 5:21 ` Niklas Holsti
1 sibling, 3 replies; 202+ messages in thread
From: Robert A Duff @ 2013-05-12 22:15 UTC (permalink / raw)
Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org> writes:
> I'm not sure I see the point in having an object for a closed file,
Yeah, I was about to post basically the same thing. A closed file
is pretty useless. It's like an uninitialized variable -- you can't
do anything with it.
> other than the requirements of low-level languages in which such things
> were 1st implemented.
Low-level languages like Ada 83? ;-)
>...Why not something like
>
> type File_Info (<>) is tagged limited private;
Yes, but I would have separate types for Input_File and Output_File.
Possibly another type for the rare case when you want to
read and write to/from the same file handle.
> function Open (Name : ...; ...) return File_Info;
> function Create (Name : ...; ...) return File_Info;
Note that these are build-in-place functions. You can't call them
as the right-hand side of an assignment statement.
> function Read (File : in out File_Info) return ...;
> procedure Write (File : in out File_Info; Item : in ...);
>
> declare
> File : File_Info := Open ("junk", ...);
> begin
> Data := Read (File);
> ...
> end;
You could use it as above, or like this:
Grind_Upon_File(Open("junk", ...));
Or like this:
X := new File_Info'(Open(...));
But you couldn't use it like this:
File : File_Info; -- Illegal!
... -- some code that computes File_Name
File := Open (File_Name); -- Illegal!
which is a limitation, compared to the current design of Text_IO
and friends.
> A File_Info must be opened or created when declared, and is closed when
> it's finalized.
Right.
- Bob
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-12 22:15 ` Robert A Duff
@ 2013-05-13 0:26 ` Jeffrey Carter
2013-05-13 7:03 ` Yannick Duchêne (Hibou57)
2013-05-14 2:14 ` Randy Brukardt
2 siblings, 0 replies; 202+ messages in thread
From: Jeffrey Carter @ 2013-05-13 0:26 UTC (permalink / raw)
On 05/12/2013 03:15 PM, Robert A Duff wrote:
> Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org> writes:
>
>> I'm not sure I see the point in having an object for a closed file,
>
> Yeah, I was about to post basically the same thing. A closed file
> is pretty useless. It's like an uninitialized variable -- you can't
> do anything with it.
>
>> other than the requirements of low-level languages in which such things
>> were 1st implemented.
>
> Low-level languages like Ada 83? ;-)
Or even Ada 80 :) But I suspect everything goes back to how files were handled
in 1950's assembly languages.
> Yes, but I would have separate types for Input_File and Output_File.
> Possibly another type for the rare case when you want to
> read and write to/from the same file handle.
Yes, that's an additional possible refinement.
> But you couldn't use it like this:
>
> File : File_Info; -- Illegal!
> ... -- some code that computes File_Name
> File := Open (File_Name); -- Illegal!
>
> which is a limitation, compared to the current design of Text_IO
> and friends.
That's what block statements are for.
--
Jeff Carter
"I fart in your general direction."
Monty Python & the Holy Grail
05
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-12 22:15 ` Robert A Duff
2013-05-13 0:26 ` Jeffrey Carter
@ 2013-05-13 7:03 ` Yannick Duchêne (Hibou57)
2013-05-13 13:15 ` Robert A Duff
2013-05-14 2:14 ` Randy Brukardt
2 siblings, 1 reply; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-13 7:03 UTC (permalink / raw)
Le Mon, 13 May 2013 00:15:24 +0200, Robert A Duff
<bobduff@shell01.theworld.com> a écrit:
> Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org> writes:
>
>> I'm not sure I see the point in having an object for a closed file,
>
> Yeah, I was about to post basically the same thing. A closed file
> is pretty useless.
As said Niklas, the initial idea was requirements on the state of objects
for some operation to occur or not occur.
Just on the object for a closed file, this make sense if the object does
not really disappear when it is closed. If the object still exist in scope
or via kind of references, it needs to have a `Closed` state. That would
not be the same if the file would be automatically closed when going out
of scope and always be opened when appearing in the scope.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-13 7:03 ` Yannick Duchêne (Hibou57)
@ 2013-05-13 13:15 ` Robert A Duff
2013-05-13 17:30 ` Jeffrey Carter
0 siblings, 1 reply; 202+ messages in thread
From: Robert A Duff @ 2013-05-13 13:15 UTC (permalink / raw)
"Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr> writes:
> As said Niklas, the initial idea was requirements on the state of
> objects for some operation to occur or not occur.
Yes, I understood that. I just don't think "open/closed file" is
the best example. Maybe something like, you can't do the "land
aircraft" operation unless you're in the "landing gear down" state.
By the way, Text_IO has more design flaws than I can count without
taking off my shoes. ;-)
- Bob
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-13 13:15 ` Robert A Duff
@ 2013-05-13 17:30 ` Jeffrey Carter
2013-05-13 18:01 ` J-P. Rosen
0 siblings, 1 reply; 202+ messages in thread
From: Jeffrey Carter @ 2013-05-13 17:30 UTC (permalink / raw)
On 05/13/2013 06:15 AM, Robert A Duff wrote:
>
> Yes, I understood that. I just don't think "open/closed file" is
> the best example. Maybe something like, you can't do the "land
> aircraft" operation unless you're in the "landing gear down" state.
Sure you can. It happens all the time. There are 2 kinds of pilots who fly
retractable-gear airplanes: those who have made a gear-up landing, and those who
will.
> By the way, Text_IO has more design flaws than I can count without
> taking off my shoes. ;-)
All the file handling seems poorly designed. I would only have 1 file type (or a
few, for input, output, and input-output files), for example, with different
levels of operations on them. It seems ridiculous to have different File_Type's
declared for Stream, Direct, and Text access to files.
--
Jeff Carter
"People called Romanes, they go the house?"
Monty Python's Life of Brian
79
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-13 17:30 ` Jeffrey Carter
@ 2013-05-13 18:01 ` J-P. Rosen
2013-05-13 18:39 ` Bill Findlay
` (2 more replies)
0 siblings, 3 replies; 202+ messages in thread
From: J-P. Rosen @ 2013-05-13 18:01 UTC (permalink / raw)
Le 13/05/2013 19:30, Jeffrey Carter a écrit :
> All the file handling seems poorly designed. I would only have 1 file
> type (or a few, for input, output, and input-output files), for example,
> with different levels of operations on them. It seems ridiculous to have
> different File_Type's declared for Stream, Direct, and Text access to
> files.
Because you are used to poor operating systems like Unix and Windows,
where files are simply a raw bag of bytes.
In the old times, when people still knew how to write OSes (VMS...), you
had various kinds of files that were managed at OS level. A sequential
file was the logical mapping for a tape, and a direct file for a disc.
--
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-13 18:01 ` J-P. Rosen
@ 2013-05-13 18:39 ` Bill Findlay
2013-05-13 18:57 ` Jeffrey Carter
2013-05-13 19:13 ` Robert A Duff
2 siblings, 0 replies; 202+ messages in thread
From: Bill Findlay @ 2013-05-13 18:39 UTC (permalink / raw)
On 13/05/2013 19:01, in article kmr9ja$40g$1@dont-email.me, "J-P. Rosen"
<rosen@adalog.fr> wrote:
> Le 13/05/2013 19:30, Jeffrey Carter a écrit :
>> All the file handling seems poorly designed. I would only have 1 file
>> type (or a few, for input, output, and input-output files), for example,
>> with different levels of operations on them. It seems ridiculous to have
>> different File_Type's declared for Stream, Direct, and Text access to
>> files.
> Because you are used to poor operating systems like Unix and Windows,
> where files are simply a raw bag of bytes.
>
> In the old times, when people still knew how to write OSes (VMS...), you
> had various kinds of files that were managed at OS level. A sequential
> file was the logical mapping for a tape, and a direct file for a disc.
Yes, and a complete pain in the neck it was too.
--
Bill Findlay
with blueyonder.co.uk;
use surname & forename;
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-13 18:01 ` J-P. Rosen
2013-05-13 18:39 ` Bill Findlay
@ 2013-05-13 18:57 ` Jeffrey Carter
2013-05-13 19:13 ` Robert A Duff
2 siblings, 0 replies; 202+ messages in thread
From: Jeffrey Carter @ 2013-05-13 18:57 UTC (permalink / raw)
On 05/13/2013 11:01 AM, J-P. Rosen wrote:
>
> In the old times, when people still knew how to write OSes (VMS...), you
> had various kinds of files that were managed at OS level. A sequential
> file was the logical mapping for a tape, and a direct file for a disc.
Those are implementation details. They should not drive the design of high-level
abstractions.
--
Jeff Carter
"People called Romanes, they go the house?"
Monty Python's Life of Brian
79
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-13 18:01 ` J-P. Rosen
2013-05-13 18:39 ` Bill Findlay
2013-05-13 18:57 ` Jeffrey Carter
@ 2013-05-13 19:13 ` Robert A Duff
2013-05-13 20:38 ` J-P. Rosen
2 siblings, 1 reply; 202+ messages in thread
From: Robert A Duff @ 2013-05-13 19:13 UTC (permalink / raw)
"J-P. Rosen" <rosen@adalog.fr> writes:
> Because you are used to poor operating systems like Unix and Windows,
> where files are simply a raw bag of bytes.
"sequence", not "bag".
> In the old times, when people still knew how to write OSes (VMS...), you
> had various kinds of files that were managed at OS level. A sequential
> file was the logical mapping for a tape, and a direct file for a disc.
I haven't used VMS in years, but I recall Record Management Services
being a nightmare! Far more complexity than could possibly be worth
the functionality provided.
Anyway, I don't see VMS (etc) being a good excuse for the design
flaws of Text_IO, because Text_IO doesn't match VMS particularly
well.
Text_IO ought to provide simple streams-of-characters abstractions,
and what it looks like on the disk, or what it looks like to the
OS should be hidden at that level.
- Bob
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-13 19:13 ` Robert A Duff
@ 2013-05-13 20:38 ` J-P. Rosen
2013-05-14 7:26 ` Dmitry A. Kazakov
2013-05-14 19:56 ` Robert A Duff
0 siblings, 2 replies; 202+ messages in thread
From: J-P. Rosen @ 2013-05-13 20:38 UTC (permalink / raw)
Le 13/05/2013 21:13, Robert A Duff a écrit :
> I haven't used VMS in years, but I recall Record Management Services
> being a nightmare! Far more complexity than could possibly be worth
> the functionality provided.
>
Maybe you used it from C... I remember VMS had to invent new access
methods specifically for C, because the VMS view of a file was too high
level for C.
> Text_IO ought to provide simple streams-of-characters abstractions,
> and what it looks like on the disk, or what it looks like to the
> OS should be hidden at that level.
Sorry, but I see a stream of characters as a lower level abstraction
than an organised sequence of pages, lines, and individual characters
(not that I am especially fan of pages)
--
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-13 20:38 ` J-P. Rosen
@ 2013-05-14 7:26 ` Dmitry A. Kazakov
2013-05-14 20:00 ` Robert A Duff
2013-05-14 19:56 ` Robert A Duff
1 sibling, 1 reply; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-14 7:26 UTC (permalink / raw)
On Mon, 13 May 2013 22:38:43 +0200, J-P. Rosen wrote:
> Le 13/05/2013 21:13, Robert A Duff a écrit :
>> I haven't used VMS in years, but I recall Record Management Services
>> being a nightmare! Far more complexity than could possibly be worth
>> the functionality provided.
>>
> Maybe you used it from C... I remember VMS had to invent new access
> methods specifically for C, because the VMS view of a file was too high
> level for C.
>
>> Text_IO ought to provide simple streams-of-characters abstractions,
>> and what it looks like on the disk, or what it looks like to the
>> OS should be hidden at that level.
> Sorry, but I see a stream of characters as a lower level abstraction
> than an organised sequence of pages, lines, and individual characters
> (not that I am especially fan of pages)
Exactly.
IMO, RSX and VMS were precursors of type-safe (one could say an OO) file
system which never came to life.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-14 7:26 ` Dmitry A. Kazakov
@ 2013-05-14 20:00 ` Robert A Duff
2013-05-15 10:10 ` Dmitry A. Kazakov
0 siblings, 1 reply; 202+ messages in thread
From: Robert A Duff @ 2013-05-14 20:00 UTC (permalink / raw)
"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> IMO, RSX and VMS were precursors of type-safe (one could say an OO) file
> system which never came to life.
I'd love to see a type-safe file system. I've thought a lot about
how to design such a thing, and I don't think it's easy. Ada types
don't work, because they vanish when the program exits, whereas files
out-live programs.
And I don't see VMS files as being a good basis for that. If they're
the "precursor" as you say, they are extremely primitive. And yet
super complicated.
I never used RSX-11.
- Bob
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-14 20:00 ` Robert A Duff
@ 2013-05-15 10:10 ` Dmitry A. Kazakov
0 siblings, 0 replies; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-15 10:10 UTC (permalink / raw)
On Tue, 14 May 2013 16:00:46 -0400, Robert A Duff wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>
>> IMO, RSX and VMS were precursors of type-safe (one could say an OO) file
>> system which never came to life.
>
> I'd love to see a type-safe file system. I've thought a lot about
> how to design such a thing, and I don't think it's easy. Ada types
> don't work, because they vanish when the program exits, whereas files
> out-live programs.
They would continue to live in the OS. Files could be viewed as persistent
objects.
I agree that in existing Ada would be difficult, because it does not
properly separate representation, which you would like to be able to change
as the OS evolves. E.g. record members should be operations etc.
Then Ada lacks protection against intentional misuse. It should allow
making private stuff memory protected.
There are general issues with typed OS interfaces. E.g. when putting stuff
into a DLL, it does not work well unless drastically limited to very
primitive set of subprograms and basic types like int and char *.
I think that CS in general is not ready for this, as any innovation in the
area of OS design was trumped down by Linux and Windows for decades. The
focus was shifted to services and garbage protocols.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-13 20:38 ` J-P. Rosen
2013-05-14 7:26 ` Dmitry A. Kazakov
@ 2013-05-14 19:56 ` Robert A Duff
2013-05-15 4:24 ` Yannick Duchêne (Hibou57)
2013-05-15 14:21 ` J-P. Rosen
1 sibling, 2 replies; 202+ messages in thread
From: Robert A Duff @ 2013-05-14 19:56 UTC (permalink / raw)
"J-P. Rosen" <rosen@adalog.fr> writes:
> Le 13/05/2013 21:13, Robert A Duff a écrit :
>> I haven't used VMS in years, but I recall Record Management Services
>> being a nightmare! Far more complexity than could possibly be worth
>> the functionality provided.
>>
> Maybe you used it from C...
No, I don't recall writing any C on VMS. On Unix, Windows,
misc embedded systems, yes, but not on VMS.
On VMS I mainly used Pascal, with a little bit of assembly.
Pascal I/O is also poorly designed, by the way, which is
probably why I was horsing around with RMS. Text I/O in Java
or Lisp, for example, is superior to either C or Ada, IMHO.
>... I remember VMS had to invent new access
> methods specifically for C, because the VMS view of a file was too high
> level for C.
Interesting. I don't see why -- VMS files can represent a
"sequence of bytes", among other things.
>> Text_IO ought to provide simple streams-of-characters abstractions,
>> and what it looks like on the disk, or what it looks like to the
>> OS should be hidden at that level.
> Sorry, but I see a stream of characters as a lower level abstraction
> than an organised sequence of pages, lines, and individual characters
> (not that I am especially fan of pages)
OK, let's agree that pages are junk.
That leaves "sequence of lines, each of which is a sequence of
characters". Some programs do indeed want to view text that way. But
Text_IO doesn't support that very conveniently. There isn't even a Line
type in Ada. And the Get_Line procedure requires a fixed-length string,
and the length of that string is guaranteed to be both too short and too
long. (I'm talking about flaws in the original design, here, so Ada 83
-- I realize a Get_Line function was later added.) So the design
encourages the sort of broken program that doesn't work right when there
are long lines. There are lots of C programs with the same kind of bug,
for similar reasons.
And there's no data type in Ada that can portably represent a multi-line
piece of text. Of course, you can build your own, but something so
basic ought to be predefined.
Furthermore, lots of programs do NOT want that two-level structure.
They just want a sequence of characters, with one (not two!)
particular character that means "line break". They want to have
code like:
... loop
case Current_Char is
...
where a line break is treated similarly (or identically)
to ' '. The GNAT front end is like that (the lexical
analysis, I mean), and it doesn't use Text_IO to read the
source text.
- Bob
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-14 19:56 ` Robert A Duff
@ 2013-05-15 4:24 ` Yannick Duchêne (Hibou57)
2013-05-15 9:28 ` Dmitry A. Kazakov
2013-05-15 14:21 ` J-P. Rosen
1 sibling, 1 reply; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-15 4:24 UTC (permalink / raw)
Le Tue, 14 May 2013 21:56:14 +0200, Robert A Duff
<bobduff@shell01.theworld.com> a écrit:
> Furthermore, lots of programs do NOT want that two-level structure.
> They just want a sequence of characters, with one (not two!)
> particular character that means "line break". They want to have
> code like:
>
> ... loop
> case Current_Char is
> ...
That's a corner case, and why Ada should do pre‑tokenization for this
single case? If end‑of‑line is made of two characters in some
environments, then the end of line token is not a character, or else it's
a character in a kind of internal character set (what most people surely
do, indeed, and that's out of the standard).
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-15 4:24 ` Yannick Duchêne (Hibou57)
@ 2013-05-15 9:28 ` Dmitry A. Kazakov
2013-05-15 11:31 ` Peter C. Chapin
0 siblings, 1 reply; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-15 9:28 UTC (permalink / raw)
On Wed, 15 May 2013 06:24:49 +0200, Yannick Duchêne (Hibou57) wrote:
> Le Tue, 14 May 2013 21:56:14 +0200, Robert A Duff
> <bobduff@shell01.theworld.com> a écrit:
>> Furthermore, lots of programs do NOT want that two-level structure.
>> They just want a sequence of characters, with one (not two!)
>> particular character that means "line break". They want to have
>> code like:
>>
>> ... loop
>> case Current_Char is
>> ...
>
> That's a corner case, and why Ada should do pre‑tokenization for this
> single case?
It is not a tokenization. You turned abstraction upside down. The text file
is a sequence of lines. A line is a sequence of characters. Period.
If you have a broken OS, like Linux/Windows is, you cannot have this
abstraction. Instead you emulate it as a lower-level stream of octets with
escape sequences used to simulate lines. What is wrong with that? It
conflates representation with the interface.
> If end‑of‑line is made of two characters in some
> environments, then the end of line token is not a character, or else it's
> a character in a kind of internal character set (what most people surely
> do, indeed, and that's out of the standard).
It is not how it was under VMS. It did not have such stuff in record
oriented files. Such files had each line kept with the character count. It
was not a stream of characters. Though under VMS you could read it as a
stream of octets if you wanted.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-15 9:28 ` Dmitry A. Kazakov
@ 2013-05-15 11:31 ` Peter C. Chapin
2013-05-15 12:32 ` Yannick Duchêne (Hibou57)
` (2 more replies)
0 siblings, 3 replies; 202+ messages in thread
From: Peter C. Chapin @ 2013-05-15 11:31 UTC (permalink / raw)
On Wed, 15 May 2013, Dmitry A. Kazakov wrote:
> If you have a broken OS, like Linux/Windows is, you cannot have this
> abstraction. Instead you emulate it as a lower-level stream of octets
> with escape sequences used to simulate lines. What is wrong with that?
> It conflates representation with the interface.
The genius of the Linux (and Windows) way of representing files is that
the operating system does not need to know anything about the nature of
the data being stored in the files. Thus new file types can be defined by
applications without any OS changes. This does push the burden of
interpreting the file's format into the application but the benefit is a
more generic operating system. When one considers all the different kinds
of files created by applications today, I can't imagine any other way
working well.
Peter
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-15 11:31 ` Peter C. Chapin
@ 2013-05-15 12:32 ` Yannick Duchêne (Hibou57)
2013-05-15 19:59 ` Peter C. Chapin
2013-05-15 12:46 ` Dmitry A. Kazakov
2013-05-15 18:15 ` Jeffrey Carter
2 siblings, 1 reply; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-15 12:32 UTC (permalink / raw)
Le Wed, 15 May 2013 13:31:36 +0200, Peter C. Chapin <PChapin@vtc.vsc.edu>
a écrit:
> The genius of the Linux (and Windows) way of representing files is that
> the operating system does not need to know anything about the nature of
> the data being stored in the files. Thus new file types can be defined
> by applications without any OS changes. This does push the burden of
> interpreting the file's format into the application but the benefit is a
> more generic operating system. When one considers all the different
> kinds of files created by applications today, I can't imagine any other
> way working well.
I may see a better options: what about multiple views for a file? File
view drivers? Query interface to query what interface(s)/view(s) a file
provides? A standard format to describe interfaces? Standardisation of a
basic set of very common interface (which may be completed as the
technologies evolves)?
Pushing this kind of responsibility to the applications, is the surest way
to have a mess of non‑interoperable things, wasting duplicates,
inconsistencies, data corruption, applications guessing all the time, etc
(and that's indeed how it goes so far). Just imagine what if each
applications was responsible of accessing devices or managing memory
pages. The comparison is not that much excessive: nor POSIX nor Linux
provides anything for mandatory locks on files (at least, Windows is
cleaner on that aspect), and it only works between cooperative
applications (modulo their bugs) and can be fully ignored accidentally or
worst, on purpose, by any other application.
There is too much responsibilities left to applications in this area. The
OS discharges itself from near to everything but storage devices access
(or may be an OS is just a big device driver), which is just a way to say
it provides near to no service at all here (except a stream of raw bytes),
and each possible view must be a duplicated feature in each application
(or multiple shared and overlapping non‑standardized libraries, which ends
into others and similar issues).
Even determination of the MIME type of a file does not work well, and may
have to be fixed by some application (just think of `file` and `xdg-mime`
on Ubuntu, not always returning the same answer for a query). What the OS
or environment does not provides, each application has to duplicate it,
and may be wrong with or may miss some point.
That's one of my biggest (*) grief with OS (at least widespread OS, as I
don't known others nor old ones).
(*) Another big one is about applications each believing it's the centre
of the world, which comes with similar consequences: wasting with
duplications, inconsistencies, poor UI behaviour standardisation,
encumbered workspace, and so on.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-15 12:32 ` Yannick Duchêne (Hibou57)
@ 2013-05-15 19:59 ` Peter C. Chapin
2013-05-15 20:56 ` Dmitry A. Kazakov
0 siblings, 1 reply; 202+ messages in thread
From: Peter C. Chapin @ 2013-05-15 19:59 UTC (permalink / raw)
On Wed, 15 May 2013, Yannick Duchêne (Hibou57) wrote:
> I may see a better options: what about multiple views for a file? File
> view drivers? Query interface to query what interface(s)/view(s) a file
> provides? A standard format to describe interfaces? Standardisation of a
> basic set of very common interface (which may be completed as the
> technologies evolves)?
>
> Pushing this kind of responsibility to the applications, is the surest
> way to have a mess of non‑interoperable things, wasting duplicates,
> inconsistencies, data corruption, applications guessing all the time,
> etc (and that's indeed how it goes so far).
I understand what you're saying. The issue ultimately comes down to
deciding how high up the chain of abstraction one expects the operating
system to go. We can probably all agree that the OS should be responsible
for managing the hardware itself (via device drivers). We can also
probably all agree that the application should deal with problems that are
unique to it.
Yet who should deal with the structure of, say, a JPEG image? Should every
application that wants to manipulate such images duplicate the code
required to do so? Should the OS materialize the "JPEG file" abstraction
directly in its API?
Of course in the real world JPEG images are manipulated by a library that
multiple applications can use. Thus while the code *is* duplicated in
each process as far as the OS can see, the programmers are not really
writing that code freshly every time. In fact, in many systems that code
could reside in a shared library... a kind of gray zone between the
application and the OS.
Any OS that tried to provide a specialized JPEG file type is biting off a
lot. It would be taking on the responsibility of providing every kind of
specialized file type that could ever exist. To do that it would have to
provide a low level "sequence of bytes" abstraction along with some kind
of extension mechanism (shared libraries?) to allow users to add on the
support they need.
Isn't that what we have now, more or less?
Peter
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-15 19:59 ` Peter C. Chapin
@ 2013-05-15 20:56 ` Dmitry A. Kazakov
0 siblings, 0 replies; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-15 20:56 UTC (permalink / raw)
On Wed, 15 May 2013 15:59:07 -0400, Peter C. Chapin wrote:
> Yet who should deal with the structure of, say, a JPEG image?
The implementation of the type if the OS were typed.
> Should every
> application that wants to manipulate such images duplicate the code
> required to do so?
The operations of the type could be shared.
> Should the OS materialize the "JPEG file" abstraction
> directly in its API?
JPEG would implement the interface of some base image type.
It is not much different from how OSes handle drivers. You can register new
driver. A driver belongs to a class of devices (=implements some device
interface, e.g. block device).
The API of a driver is a kind of dispatching operation, e.g.
Read/Write/Open/Close/IOCTL. It is very rudimental and not properly defined
as a type, nonetheless.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-15 11:31 ` Peter C. Chapin
2013-05-15 12:32 ` Yannick Duchêne (Hibou57)
@ 2013-05-15 12:46 ` Dmitry A. Kazakov
2013-05-15 18:15 ` Jeffrey Carter
2 siblings, 0 replies; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-15 12:46 UTC (permalink / raw)
On Wed, 15 May 2013 07:31:36 -0400, Peter C. Chapin wrote:
> On Wed, 15 May 2013, Dmitry A. Kazakov wrote:
>
>> If you have a broken OS, like Linux/Windows is, you cannot have this
>> abstraction. Instead you emulate it as a lower-level stream of octets
>> with escape sequences used to simulate lines. What is wrong with that?
>> It conflates representation with the interface.
>
> The genius of the Linux (and Windows) way of representing files is that
> the operating system does not need to know anything about the nature of
> the data being stored in the files.
E.g. in order to execute it. Right?
> Thus new file types can be defined by
> applications without any OS changes. This does push the burden of
> interpreting the file's format into the application but the benefit is a
> more generic operating system.
Viruses and performance that makes i7 to perform as i486.
> When one considers all the different kinds
> of files created by applications today, I can't imagine any other way
> working well.
A much more efficient, safer, compacter system?
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-15 11:31 ` Peter C. Chapin
2013-05-15 12:32 ` Yannick Duchêne (Hibou57)
2013-05-15 12:46 ` Dmitry A. Kazakov
@ 2013-05-15 18:15 ` Jeffrey Carter
2013-05-15 19:18 ` Eryndlia Mavourneen
2 siblings, 1 reply; 202+ messages in thread
From: Jeffrey Carter @ 2013-05-15 18:15 UTC (permalink / raw)
On 05/15/2013 04:31 AM, Peter C. Chapin wrote:
>
> The genius of the Linux (and Windows) way of representing files is that the
> operating system does not need to know anything about the nature of the data
> being stored in the files. Thus new file types can be defined by applications
> without any OS changes. This does push the burden of interpreting the file's
> format into the application but the benefit is a more generic operating system.
> When one considers all the different kinds of files created by applications
> today, I can't imagine any other way working well.
Ada 83 had a philosophy of providing building blocks and letting the user use
them to create what he wants. The language provided the means to create
mathematical functions and unbounded arrays and queues and sets, so the language
did not provide such things. This resulted in a proliferation of external
libraries and negative comparisons to languages with large standard libraries.
In 1995 Ada was revised to include some of these things, and again in 2007 more
of them, including hashed and ordered maps and sets, but the underlying building
blocks of an O(log N) searchable structure and a hash table were not provided to
the user. This represents the opposite philosophy to that of Ada 83: providing
high-level abstractions but not the building blocks to build them.
(Of course, Ada 83 required a compiler implementer to have a bignum package, but
not to make it available to users of the compiler, so the difference is not as
clear as I'm pretending.)
Between these 2 extremes is a philosophy of providing building blocks and common
high-level abstractions build from them.
Physically, a disk is a bunch of bytes; everything else is built on top of that.
The Unix file concept provides the building blocks but no higher-level
abstractions. VMS (which, IIRC, did not initially have a sequence-of-bytes way
to access files) represented the other extreme. Presumably there are some common
higher-level file types that it would be useful to have the OS provide in
addition to the sequence-of-bytes view, just as it's useful to have a language
provide common higher-level constructs as well as the building blocks to build them.
--
Jeff Carter
"Nobody expects the Spanish Inquisition!"
Monty Python's Flying Circus
22
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-15 18:15 ` Jeffrey Carter
@ 2013-05-15 19:18 ` Eryndlia Mavourneen
2013-05-15 19:57 ` Dmitry A. Kazakov
2013-05-16 9:41 ` G.B.
0 siblings, 2 replies; 202+ messages in thread
From: Eryndlia Mavourneen @ 2013-05-15 19:18 UTC (permalink / raw)
On Wednesday, May 15, 2013 1:15:07 PM UTC-5, Jeffrey Carter wrote:
>
> Physically, a disk is a bunch of bytes; everything else is built on top of that.
>
> The Unix file concept provides the building blocks but no higher-level
> abstractions. VMS (which, IIRC, did not initially have a sequence-of-bytes way
> to access files) represented the other extreme. Presumably there are some common
> higher-level file types that it would be useful to have the OS provide in
> addition to the sequence-of-bytes view, just as it's useful to have a language
> provide common higher-level constructs as well as the building blocks to build them.
>
Actually, VMS and its predecessor RSX-11 (all flavors) provided a wide range of choices from
1) physical block/sector device I/O to
2) logical block/sector file I/O to
3) variable-sized file record structure (sequential I/O) [the size was separate from the record but did not preclude the inclusion of terminator(s) or any other characters in the record] to
4) fixed-length file record structure (sequential or direct I/O) to
5) indexed-sequential file structure (sequential or indexed I/O using 1 or more indices).
RMS (Record Management Services) represented the last 3 (3-5) of these.
These choices are so complete that for many DB applications, they are all that is needed. I have seen many personnel REQs for DB programmer or administrator that specified the DB as RMS. I have used all 5 I/O modes and did not find any of them particularly difficult or cumbersome to use. Even more so with Ada.
DEC's layered product Rdb provided for true relational DB capability.
Btw, VMS is still maintained and upgraded by HP.
[As an addendum -- I used DEC Ada and preferred it in some ways over Gnat. Error messages are the main thing that comes to mind. DEC Ada didn't just give you the error message but cross-referenced it to the specific LRM paragraph(s) that dealt with the situation. Very helpful.]
Eryndlia Mavourneen
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-15 19:18 ` Eryndlia Mavourneen
@ 2013-05-15 19:57 ` Dmitry A. Kazakov
2013-05-15 20:37 ` Yannick Duchêne (Hibou57)
2013-05-16 9:41 ` G.B.
1 sibling, 1 reply; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-15 19:57 UTC (permalink / raw)
On Wed, 15 May 2013 12:18:34 -0700 (PDT), Eryndlia Mavourneen wrote:
> [As an addendum -- I used DEC Ada and preferred it in some ways over Gnat.
> Error messages are the main thing that comes to mind. DEC Ada didn't just
> give you the error message but cross-referenced it to the specific LRM
> paragraph(s) that dealt with the situation. Very helpful.]
Me too. DEC Ada was a great compiler as well as DEC C.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-15 19:57 ` Dmitry A. Kazakov
@ 2013-05-15 20:37 ` Yannick Duchêne (Hibou57)
2013-05-15 20:48 ` Dmitry A. Kazakov
0 siblings, 1 reply; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-15 20:37 UTC (permalink / raw)
Le Wed, 15 May 2013 21:57:57 +0200, Dmitry A. Kazakov
<mailbox@dmitry-kazakov.de> a écrit:
> Me too. DEC Ada was a great compiler as well as DEC C.
What version of Ada does/did it support? Ada 95? Ada 2005? Why do you say
“was”?
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-15 20:37 ` Yannick Duchêne (Hibou57)
@ 2013-05-15 20:48 ` Dmitry A. Kazakov
2013-05-16 12:45 ` Eryndlia Mavourneen
0 siblings, 1 reply; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-15 20:48 UTC (permalink / raw)
On Wed, 15 May 2013 22:37:46 +0200, Yannick Duchêne (Hibou57) wrote:
> Le Wed, 15 May 2013 21:57:57 +0200, Dmitry A. Kazakov
> <mailbox@dmitry-kazakov.de> a écrit:
>
>> Me too. DEC Ada was a great compiler as well as DEC C.
>
> What version of Ada does/did it support? Ada 95? Ada 2005?
Ada 83
> Why do you say “was”?
DEC is dead.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-15 20:48 ` Dmitry A. Kazakov
@ 2013-05-16 12:45 ` Eryndlia Mavourneen
2013-05-16 17:16 ` Jeffrey Carter
0 siblings, 1 reply; 202+ messages in thread
From: Eryndlia Mavourneen @ 2013-05-16 12:45 UTC (permalink / raw)
On Wednesday, May 15, 2013 3:48:35 PM UTC-5, Dmitry A. Kazakov wrote:
> On Wed, 15 May 2013 22:37:46 +0200, Yannick Duchêne (Hibou57) wrote:
> > Le Wed, 15 May 2013 21:57:57 +0200, Dmitry A. Kazakov
> > <mailbox@dmitry-kazakov.de> a écrit:
>
>> Me too. DEC Ada was a great compiler as well as DEC C.
>
> > What version of Ada does/did it support? Ada 95? Ada 2005?
>
> Ada 83
>
> > Why do you say “was”?
>
> DEC is dead.
When VMS and the hardware it runs on (VAX and Alpha) were picked up by HP, HP dropped DEC Ada and adopted the VMS version of Gnat.
Eryndlia Mavourneen
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-16 12:45 ` Eryndlia Mavourneen
@ 2013-05-16 17:16 ` Jeffrey Carter
0 siblings, 0 replies; 202+ messages in thread
From: Jeffrey Carter @ 2013-05-16 17:16 UTC (permalink / raw)
On 05/16/2013 05:45 AM, Eryndlia Mavourneen wrote:
>
> When VMS and the hardware it runs on (VAX and Alpha) were picked up by HP, HP
> dropped DEC Ada and adopted the VMS version of Gnat.
GNAT contains many features to make it compatible with DEC Ada programs that use
implementation-dependent features of DEC Ada. An example is pragma Passive;
others may be found by searching for "DEC Ada" in the GNAT RM. These exist
because AdaCore received a contract to supply a version of GNAT as the VMS
Ada-95 compiler, with the requirement that it accept all
implementation-dependent features of DEC Ada.
I once used GNAT in Ada-83 mode as the development compiler for a system that
was compiled using DEC Ada and run on VAX/VMS.
--
Jeff Carter
"I'm a kike, a yid, a heebie, a hook nose! I'm Kosher,
Mum! I'm a Red Sea pedestrian, and proud of it!"
Monty Python's Life of Brian
77
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-15 19:18 ` Eryndlia Mavourneen
2013-05-15 19:57 ` Dmitry A. Kazakov
@ 2013-05-16 9:41 ` G.B.
2013-05-16 12:35 ` J-P. Rosen
1 sibling, 1 reply; 202+ messages in thread
From: G.B. @ 2013-05-16 9:41 UTC (permalink / raw)
> [As an addendum -- I used DEC Ada and preferred it in some ways over Gnat. Error messages are the main thing that comes to mind. DEC Ada didn't just give you the error message but cross-referenced it to the specific LRM paragraph(s) that dealt with the situation. Very helpful.]
Compilers using AdaMagic as their front end frequently
reference the LRM in error messages. Now that SofCheck,
maker of AdaMagic, has joined AdaCore, maybe GNAT will
more frequently do so, too, rather than just re-using
LRM terms in disguise, as in
"invalid prefix in selected component"
This error message is not about the component.
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-16 9:41 ` G.B.
@ 2013-05-16 12:35 ` J-P. Rosen
0 siblings, 0 replies; 202+ messages in thread
From: J-P. Rosen @ 2013-05-16 12:35 UTC (permalink / raw)
Le 16/05/2013 11:41, G.B. a �crit :
> Compilers using AdaMagic as their front end frequently
> reference the LRM in error messages. Now that SofCheck,
> maker of AdaMagic, has joined AdaCore, maybe GNAT will
> more frequently do so, too
I doubt it.
All Ada83 compilers were referencing the LRM. It was a deliberate
decision of the Gnat authors not to do so, because they felt that in
many cases, it was more confusing than helpful. In a few cases where a
reference is really needed, Gnat does output the reference. But not for
"missing semi-colon", as other compilers did.
--
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-14 19:56 ` Robert A Duff
2013-05-15 4:24 ` Yannick Duchêne (Hibou57)
@ 2013-05-15 14:21 ` J-P. Rosen
1 sibling, 0 replies; 202+ messages in thread
From: J-P. Rosen @ 2013-05-15 14:21 UTC (permalink / raw)
Le 14/05/2013 21:56, Robert A Duff a �crit :
> "J-P. Rosen" <rosen@adalog.fr> writes:
>> ... I remember VMS had to invent new access
>> methods specifically for C, because the VMS view of a file was too high
>> level for C.
>
> Interesting. I don't see why -- VMS files can represent a
> "sequence of bytes", among other things.
It was long ago, but AFAIR, VMS had several forms of structured files,
that were very inconvenient for C - DEC added another one later for raw
bytes
> [...] And the Get_Line procedure requires a fixed-length string,
> and the length of that string is guaranteed to be both too short and too
> long. (I'm talking about flaws in the original design, here, so Ada 83
> -- I realize a Get_Line function was later added.)
I have written my own Get_Line function, which is perfectly Ada-83
compatible. True enough, the Ada-83 mantra was "Ada is so powerful, you
can write anything you need" - and then people complained that they had
to rewrite everything. That's why the library was considerably increased
later on. But on the principle, dealing with long lines was not really a
problem, and did not require buffers of arbitrary limited size.
> [...]
> Furthermore, lots of programs do NOT want that two-level structure.
> They just want a sequence of characters, with one (not two!)
> particular character that means "line break". They want to have
> code like:
>
> ... loop
> case Current_Char is
> ...
>
> where a line break is treated similarly (or identically)
> to ' '. The GNAT front end is like that (the lexical
> analysis, I mean), and it doesn't use Text_IO to read the
> source text.
>
The proper (and easy) way to check for the end of line is to call the
function mysteriously called End_Of_Line ;-). I don't see a problem with
that. If you want to replace end of lines with a particular character,
just write your custom Get_Char function (you'll have to write it anyway
to manage look-ahead characters).
On the opposite, I don't like languages that invent characters on the
fly. In Ada, you read the characters that are in the file. The end of
line is not a character in a sufficiently evolved operating system.
--
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-12 22:15 ` Robert A Duff
2013-05-13 0:26 ` Jeffrey Carter
2013-05-13 7:03 ` Yannick Duchêne (Hibou57)
@ 2013-05-14 2:14 ` Randy Brukardt
2013-05-14 19:35 ` Robert A Duff
2 siblings, 1 reply; 202+ messages in thread
From: Randy Brukardt @ 2013-05-14 2:14 UTC (permalink / raw)
"Robert A Duff" <bobduff@shell01.TheWorld.com> wrote in message
news:wccmwrzu9oj.fsf@shell01.TheWorld.com...
> Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org> writes:
>
>> I'm not sure I see the point in having an object for a closed file,
>
> Yeah, I was about to post basically the same thing. A closed file
> is pretty useless. It's like an uninitialized variable -- you can't
> do anything with it.
Yes, and of course Ada allows uninitialized variables, too. Clearly the same
sorts of reasons apply.
We briefly tried that model when designing Claw, but it really didn't work,
because the underlying handle can be closed by some other operation and in
that case the object becomes closed (we called it "invalid") without any
explicit action in your code. For a windowing system, that other operation
can be the guy with the mouse, who can easily screw up all of your carefully
thought out code.
Another issue is that doing that means that you are limited to Ada's scopes
for managing objects, which means that you're limited in how you can set up
and tear down structures. (You can always get around those problems by
essentially making your clients use new/unchecked_deallocation for
everything -- but I don't consider that a step forward. I'd rather have
"invalid" objects than force people to use access types.)
We used that model throughout Claw, and that included in Claw.Directories,
so of course it carried over into the original proposal for Ada.Directories
(which was heavily based on Claw.Directories). So "Search_Type" originally
had a "Is_Valid" routine, which eventually got folded into "More_Entries".
(Which demonstrates an intermediate approach that often works -- have a
default initial state which is well-defined but not useful.)
Randy.
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-14 2:14 ` Randy Brukardt
@ 2013-05-14 19:35 ` Robert A Duff
2013-05-15 4:11 ` Yannick Duchêne (Hibou57)
2013-05-16 23:36 ` Randy Brukardt
0 siblings, 2 replies; 202+ messages in thread
From: Robert A Duff @ 2013-05-14 19:35 UTC (permalink / raw)
"Randy Brukardt" <randy@rrsoftware.com> writes:
> Yes, and of course Ada allows uninitialized variables, too. Clearly the same
> sorts of reasons apply.
Yes. I think what's missing is an ability to initialize an object
after creating it (either by declaring it, or via "new"). My hobby
language has that. And it distinguishes syntactically between
initialization and assignment_statement.
Ada uses ":=" for both, so if you do:
F : constant File_Type; -- Illegal!
... -- calculate File_Name
F := Open (File_Name); -- Illegal!
that last statement is an assignment_statement in Ada, whereas it
is conceptually an initialization. (That's illegal in Ada, because
F is declared 'constant'. You can erase 'constant', but it's STILL
illegal, because File_Type is a build-in-place limited type.)
> We briefly tried that model when designing Claw, but it really didn't work,
> because the underlying handle can be closed by some other operation and in
> that case the object becomes closed (we called it "invalid") without any
> explicit action in your code. For a windowing system, that other operation
> can be the guy with the mouse, who can easily screw up all of your carefully
> thought out code.
So how does it work in CLAW? Are you talking about some task
writing into a window, while the user is asynchronously clicking
on "close window"? So that task must be constantly checking
Is_Open (or handling an exception), and locking things to make
sure there are no race conditions?
> Another issue is that doing that means that you are limited to Ada's scopes
> for managing objects, which means that you're limited in how you can set up
> and tear down structures.
I think allowing to separate initialization from declaration
can solve that.
>...(You can always get around those problems by
> essentially making your clients use new/unchecked_deallocation for
> everything -- but I don't consider that a step forward. I'd rather have
> "invalid" objects than force people to use access types.)
Agreed -- heap allocation solves the problem, but creates other
problems.
- Bob
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-14 19:35 ` Robert A Duff
@ 2013-05-15 4:11 ` Yannick Duchêne (Hibou57)
2013-05-16 23:36 ` Randy Brukardt
1 sibling, 0 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-15 4:11 UTC (permalink / raw)
Le Tue, 14 May 2013 21:35:55 +0200, Robert A Duff
<bobduff@shell01.theworld.com> a écrit:
> Yes. I think what's missing is an ability to initialize an object
> after creating it (either by declaring it, or via "new"). My hobby
> language has that. And it distinguishes syntactically between
> initialization and assignment_statement.
> […]
> I think allowing to separate initialization from declaration
> can solve that.
Does your hobby language has static or runtime check to catch access to
uninitialized variables?
I don't see the point with deferred initialization, it seems to be an
object state finally (states, again). Either you can tell a variable was
or was not initialized, and then it has a state and it is finally
initialized before you suppose it is, or else it can't tell the variable
was not initialized because it really initialize nothing at the
declaration, and then it's perhaps unsafe.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-14 19:35 ` Robert A Duff
2013-05-15 4:11 ` Yannick Duchêne (Hibou57)
@ 2013-05-16 23:36 ` Randy Brukardt
1 sibling, 0 replies; 202+ messages in thread
From: Randy Brukardt @ 2013-05-16 23:36 UTC (permalink / raw)
"Robert A Duff" <bobduff@shell01.TheWorld.com> wrote in message
news:wcc61yl1hic.fsf@shell01.TheWorld.com...
> "Randy Brukardt" <randy@rrsoftware.com> writes:
...
>> We briefly tried that model when designing Claw, but it really didn't
>> work,
>> because the underlying handle can be closed by some other operation and
>> in
>> that case the object becomes closed (we called it "invalid") without any
>> explicit action in your code. For a windowing system, that other
>> operation
>> can be the guy with the mouse, who can easily screw up all of your
>> carefully
>> thought out code.
>
> So how does it work in CLAW? Are you talking about some task
> writing into a window, while the user is asynchronously clicking
> on "close window"? So that task must be constantly checking
> Is_Open (or handling an exception), and locking things to make
> sure there are no race conditions?
Practically, operations outside of "action routines" always have to be
prepared for an operation to raise Not_Valid_Error (with appropriate
handlers). Pretesting with Is_Valid doesn't work because it's a race
condition (that's a mistake I made in some of my early Claw programs - I
learned about the race conditions the hard way).
Claw does a lot of internal locking so that common operations are safe.
Action routines (that is, call-backs from Claw that handle action in the
GUI) lock their parameters so that they can't change state during the
execution of the routines. That eliminates a lot of problems, but in rare
instances cause deadlock (which tended to be reported as a bug in Claw -
which wasted a lot of our support time early one), so we had to used timed
locks that expire and raise a special exception (if Windows doesn't respond
in 10 seconds, there's either a deadlock or Windows itself has crashed).
I wasn't completely satisfied with the result, but of course by then we had
too many customers using Claw to change its basic design. GWindows took a
different approach, essentially requiring that only a single task can use
the GUI. I thought (and still think) that's too limiting for a language like
Ada with first-class tasking. But it does avoid the deadlock issues.
Randy.
>> Another issue is that doing that means that you are limited to Ada's
>> scopes
>> for managing objects, which means that you're limited in how you can set
>> up
>> and tear down structures.
>
> I think allowing to separate initialization from declaration
> can solve that.
>
>>...(You can always get around those problems by
>> essentially making your clients use new/unchecked_deallocation for
>> everything -- but I don't consider that a step forward. I'd rather have
>> "invalid" objects than force people to use access types.)
>
> Agreed -- heap allocation solves the problem, but creates other
> problems.
>
> - Bob
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-12 18:56 ` Jeffrey Carter
2013-05-12 22:15 ` Robert A Duff
@ 2013-05-13 5:21 ` Niklas Holsti
2013-05-13 7:22 ` Dmitry A. Kazakov
1 sibling, 1 reply; 202+ messages in thread
From: Niklas Holsti @ 2013-05-13 5:21 UTC (permalink / raw)
On 13-05-12 21:56 , Jeffrey Carter wrote:
> On 05/12/2013 01:10 AM, Niklas Holsti wrote:
>>
>> You mean like this:
>>
>> function Open (File : in Closed_File) return Open_File;
>> function Close (File : in Open_File ) return Closed_File;
>>
>> I agree that this is a possible approach. This would work, but at the
>> cost of writing the parameter/object name twice in each call:
>>
>> File : File_Object;
>> ...
>> File := Open (File);
>> File := Close (File);
>
> I'm not sure I see the point in having an object for a closed file,
> other than the requirements of low-level languages in which such things
> were 1st implemented.
This "file" stuff is only an example of a protocol that can be subjected
to typestate analysis. For "closed file", substitute "an object that is
in its initial state".
> Why not something like
>
> type File_Info (<>) is tagged limited private;
>
> function Open (Name : ...; ...) return File_Info;
> function Create (Name : ...; ...) return File_Info;
>
> function Read (File : in out File_Info) return ...;
> procedure Write (File : in out File_Info; Item : in ...);
>
> declare
> File : File_Info := Open ("junk", ...);
> begin
> Data := Read (File);
> ...
> end;
>
> A File_Info must be opened or created when declared, and is closed when
> it's finalized.
The point of the example was to illustrate typestate analysis. For this
example, with only Open - (Read/Write)* - Close, your approach collapses
the example into a trivial one, where adherence to the operation
protocol is ensured by the necessity to declare a File_Info object
before it can be used. So it would no longer be a useful example.
Your approach works in some cases, but it is problematic if you cannot
initialize the object to an "active" state in its declaration, for
example because the "activation" is conditional in some way, or must be
delayed. The "activation" must then be done in a statement, and the
declaration leaves the object in some inactive initial state.
Another limitation in your approach is that the opening and closing of
different files must be strictly nested: if you declare and open file A,
then declare and open file B, file B must be closed before file A is
closed (as long as it all happens in the same task). Such forced
constraints between the states of different object is often not wanted.
--
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
. @ .
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-13 5:21 ` Niklas Holsti
@ 2013-05-13 7:22 ` Dmitry A. Kazakov
2013-05-13 8:23 ` Yannick Duchêne (Hibou57)
2013-05-13 19:20 ` Niklas Holsti
0 siblings, 2 replies; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-13 7:22 UTC (permalink / raw)
On Mon, 13 May 2013 08:21:14 +0300, Niklas Holsti wrote:
> The point of the example was to illustrate typestate analysis. For this
> example, with only Open - (Read/Write)* - Close, your approach collapses
> the example into a trivial one, where adherence to the operation
> protocol is ensured by the necessity to declare a File_Info object
> before it can be used. So it would no longer be a useful example.
It is still a useful example of a good software component design.
> Your approach works in some cases, but it is problematic if you cannot
> initialize the object to an "active" state in its declaration, for
> example because the "activation" is conditional in some way, or must be
> delayed.
This is rather a language problem. Most of such cases can be attributed to
the lack or insufficient constructors. The notorious Ada's problem with
task components is due to the lack of class-wide constructors, when
Initialize tries to sit on two chairs struggling to be both a specific and
a class-wide initialization.
> The "activation" must then be done in a statement, and the
> declaration leaves the object in some inactive initial state.
That is not a problem so long this state is not exposed. The idea is that
when you have an object which may transit from state to state (e.g. a
connection object, when the connection can be lost), you should not expose
this state. You better make the object to maintain the state (e.g. by
making the connection restored by the object automatically) and leave its
interface free of the state (e.g. an operation on unconnected object would
block or else raise Busy_Error etc).
[ Note that here again, the precondition is relaxed to true and the
operation behavior gets defined for the exceptional state, which cannot be
avoided anyway. ]
> Another limitation in your approach is that the opening and closing of
> different files must be strictly nested: if you declare and open file A,
> then declare and open file B, file B must be closed before file A is
> closed (as long as it all happens in the same task). Such forced
> constraints between the states of different object is often not wanted.
You can have a container, e.g. a bag, to handle this.
Jeffrey's model translates this into the problem of object's scope
(lifetime), which saves time and mental efforts. Each programmer faces it
on daily basis and has his ready-to-use solutions already.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-13 7:22 ` Dmitry A. Kazakov
@ 2013-05-13 8:23 ` Yannick Duchêne (Hibou57)
2013-05-13 19:20 ` Niklas Holsti
1 sibling, 0 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-13 8:23 UTC (permalink / raw)
Le Mon, 13 May 2013 09:22:24 +0200, Dmitry A. Kazakov
<mailbox@dmitry-kazakov.de> a écrit:
>> The "activation" must then be done in a statement, and the
>> declaration leaves the object in some inactive initial state.
>
> That is not a problem so long this state is not exposed. The idea is that
> when you have an object which may transit from state to state (e.g. a
> connection object, when the connection can be lost), you should not
> expose
> this state. You better make the object to maintain the state (e.g. by
> making the connection restored by the object automatically) and leave its
> interface free of the state (e.g. an operation on unconnected object
> would
> block or else raise Busy_Error etc).
Except for the exception which implies a lot of more things, the idea is
indeed nice, while not universal. To stick with this example, that depends
on the level of the application (it may or may not be aware of possible
loss of connection), depends on the protocol in use (there may or may not
be a way to know if the connection can be restored, if it is loss of if
the peer closed it), that may be replacing a problem with another (state
vs delay), and so on.
I agree with you (or may not, depending on the concrete case), except with
this: “That is not a problem so long this state is not exposed”; this
seems to suggest another design is an error and this is an universal
pattern.
>> Another limitation in your approach is that the opening and closing of
>> different files must be strictly nested: if you declare and open file A,
>> then declare and open file B, file B must be closed before file A is
>> closed (as long as it all happens in the same task). Such forced
>> constraints between the states of different object is often not wanted.
>
> You can have a container, e.g. a bag, to handle this.
>
> Jeffrey's model translates this into the problem of object's scope
> (lifetime), which saves time and mental efforts. Each programmer faces it
> on daily basis and has his ready-to-use solutions already.
The same: may be an option, however nothing universal with it (ex. may be
too much to pull the container concept, or for the second, objects
identities may be important and one object may be opened and closed
multiple times).
There is the topic of premature optimizations, there may be as well a
topic about premature decisions (especially an issue if it adds
dependencies or complexity).
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-13 7:22 ` Dmitry A. Kazakov
2013-05-13 8:23 ` Yannick Duchêne (Hibou57)
@ 2013-05-13 19:20 ` Niklas Holsti
2013-05-14 8:14 ` Dmitry A. Kazakov
1 sibling, 1 reply; 202+ messages in thread
From: Niklas Holsti @ 2013-05-13 19:20 UTC (permalink / raw)
On 13-05-13 10:22 , Dmitry A. Kazakov wrote:
> On Mon, 13 May 2013 08:21:14 +0300, Niklas Holsti wrote:
>
>> The point of the example was to illustrate typestate analysis. For this
>> example, with only Open - (Read/Write)* - Close, your approach collapses
>> the example into a trivial one, where adherence to the operation
>> protocol is ensured by the necessity to declare a File_Info object
>> before it can be used. So it would no longer be a useful example.
>
> It is still a useful example of a good software component design.
Hm. In this thread, I think this example is interesting only if it can
show us alternatives to typestate analysis, giving the same verification
power by other means. I don't think this Open-in-declaration approach
(essentially removing the Open and Close operations from the problem)
applies in the general case, so I don't find it interesting in this thread.
>> Your approach works in some cases, but it is problematic if you cannot
>> initialize the object to an "active" state in its declaration, for
>> example because the "activation" is conditional in some way, or must be
>> delayed.
>
> This is rather a language problem. Most of such cases can be attributed to
> the lack or insufficient constructors. The notorious Ada's problem with
> task components is due to the lack of class-wide constructors, when
> Initialize tries to sit on two chairs struggling to be both a specific and
> a class-wide initialization.
The initialization step, which is just the first state transition of an
object, is only a small part of the problem for typestate analysis.
>> The "activation" must then be done in a statement, and the
>> declaration leaves the object in some inactive initial state.
>
> That is not a problem so long this state is not exposed. The idea is that
> when you have an object which may transit from state to state (e.g. a
> connection object, when the connection can be lost), you should not expose
> this state.
Even if the state is hidden from the clients, it is present internally,
and must be considered in any analysis of correctness.
> You better make the object to maintain the state (e.g. by
> making the connection restored by the object automatically) and leave its
> interface free of the state (e.g. an operation on unconnected object would
> block or else raise Busy_Error etc).
Here "unconnected object" is analogous to "closed file". The state
exists, even if hidden from clients. In fact, from the point of view of
typestate analysis, the state is or should be visible, since it affects
the availability or success of operations on the object.
The goal of typestate analysis, even of client code, is to show if
operations can be illegally applied and thus fail, for example by
raising Busy_Error. For this, the analysis must include the
"unconnected" state.
>> Another limitation in your approach is that the opening and closing of
>> different files must be strictly nested: if you declare and open file A,
>> then declare and open file B, file B must be closed before file A is
>> closed (as long as it all happens in the same task). Such forced
>> constraints between the states of different object is often not wanted.
>
> You can have a container, e.g. a bag, to handle this.
This introduces a new object -- the container -- with its own, perhaps
more complex state: whether or not it contains the object (e.g. a
File_Object) that is our real interest. Not a good idea, I think.
> Jeffrey's model translates this into the problem of object's scope
> (lifetime), which saves time and mental efforts.
Only in this special case, the "file" example, where the state structure
is so simple that after hiding the first state transition (Open) into
the construction of the object, and the last state transition (Close)
into the destruction, there is only one state left (Is_Open), which
makes typestate analysis trivial.
--
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
. @ .
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-13 19:20 ` Niklas Holsti
@ 2013-05-14 8:14 ` Dmitry A. Kazakov
0 siblings, 0 replies; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-14 8:14 UTC (permalink / raw)
On Mon, 13 May 2013 22:20:12 +0300, Niklas Holsti wrote:
> On 13-05-13 10:22 , Dmitry A. Kazakov wrote:
>> On Mon, 13 May 2013 08:21:14 +0300, Niklas Holsti wrote:
>>
>>> The point of the example was to illustrate typestate analysis. For this
>>> example, with only Open - (Read/Write)* - Close, your approach collapses
>>> the example into a trivial one, where adherence to the operation
>>> protocol is ensured by the necessity to declare a File_Info object
>>> before it can be used. So it would no longer be a useful example.
>>
>> It is still a useful example of a good software component design.
>
> Hm. In this thread, I think this example is interesting only if it can
> show us alternatives to typestate analysis, giving the same verification
> power by other means. I don't think this Open-in-declaration approach
> (essentially removing the Open and Close operations from the problem)
> applies in the general case, so I don't find it interesting in this thread.
It does. The idea is not to expose the state or else split object into
smaller ones.
>>> Your approach works in some cases, but it is problematic if you cannot
>>> initialize the object to an "active" state in its declaration, for
>>> example because the "activation" is conditional in some way, or must be
>>> delayed.
>>
>> This is rather a language problem. Most of such cases can be attributed to
>> the lack or insufficient constructors. The notorious Ada's problem with
>> task components is due to the lack of class-wide constructors, when
>> Initialize tries to sit on two chairs struggling to be both a specific and
>> a class-wide initialization.
>
> The initialization step, which is just the first state transition of an
> object, is only a small part of the problem for typestate analysis.
And the point is that this would probably be bad design.
>>> The "activation" must then be done in a statement, and the
>>> declaration leaves the object in some inactive initial state.
>>
>> That is not a problem so long this state is not exposed. The idea is that
>> when you have an object which may transit from state to state (e.g. a
>> connection object, when the connection can be lost), you should not expose
>> this state.
>
> Even if the state is hidden from the clients, it is present internally,
> and must be considered in any analysis of correctness.
But not at the client side!
>> You better make the object to maintain the state (e.g. by
>> making the connection restored by the object automatically) and leave its
>> interface free of the state (e.g. an operation on unconnected object would
>> block or else raise Busy_Error etc).
>
> Here "unconnected object" is analogous to "closed file".
No. Unconnected object can become connected asynchronously to the client.
If the state can be controlled by the client, the object should be designed
so that its sate were usable. See Jeffrey's design.
If the sate cannot be controlled the object should be responsible in each
of its states. I.e. the state should be hidden by the object
implementation.
> The state exists, even if hidden from clients.
Right. The design question is who is to control the state. You want clients
to do this. Which is distributed design overhead.
> In fact, from the point of view of
> typestate analysis, the state is or should be visible, since it affects
> the availability or success of operations on the object.
This is exactly why I consider this paradigm wrong from the design's POV.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-09 22:19 ` Randy Brukardt
2013-05-10 3:29 ` Yannick Duchêne (Hibou57)
@ 2013-05-10 3:47 ` Yannick Duchêne (Hibou57)
2013-05-11 0:22 ` Randy Brukardt
2013-05-10 3:59 ` Yannick Duchêne (Hibou57)
` (3 subsequent siblings)
5 siblings, 1 reply; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-10 3:47 UTC (permalink / raw)
Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt <randy@rrsoftware.com>
a écrit:
> 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.
Right, except while you say this, the only static check sub‑programs or
primitive operations provide, is the one applying on the types of their
arguments. So there is nothing handled by operations (at least, so far).
The point is still good enough, as at first sight, seems there are
operations which cannot said to be owned by a single type, so that may
looks hard to focus on type with this picture. Or else, there is a need
for a type representing sub‑program signature (something I wanted to reply
to Dmitry in another message), the arguments tuple, then optionally the
result tuple, and optionally both tuples, say the type of a transition as
an example. With this, interactions between types can be represented with
types.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-10 3:47 ` Yannick Duchêne (Hibou57)
@ 2013-05-11 0:22 ` Randy Brukardt
2013-05-11 7:22 ` Yannick Duchêne (Hibou57)
0 siblings, 1 reply; 202+ messages in thread
From: Randy Brukardt @ 2013-05-11 0:22 UTC (permalink / raw)
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1826 bytes --]
"Yannick Duch�ne (Hibou57)" <yannick_duchene@yahoo.fr> wrote in message
news:op.wwung605ule2fv@cardamome...
Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt <randy@rrsoftware.com>
a �crit:
>> 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.
>
>Right, except while you say this, the only static check sub-programs or
>primitive operations provide, is the one applying on the types of their
>arguments. So there is nothing handled by operations (at least, so far).
>
>The point is still good enough, as at first sight, seems there are
>operations which cannot said to be owned by a single type, so that may
>looks hard to focus on type with this picture. Or else, there is a need
>for a type representing sub-program signature (something I wanted to reply
>to Dmitry in another message), the arguments tuple, then optionally the
>result tuple, and optionally both tuples, say the type of a transition as
>an example. With this, interactions between types can be represented with
>types.
One of the reasons I chose "profile" for the name of the thingy that I was
describing on top of types was that I expected it to include profile
operations. That's because I figured that a redesign of Ada would have
first-class subprogram types; (along with subprogram objects); there is no
good reason to use explicit "access" values for this. (Object access values
are so different from the subprogram kind that there is virtually no
commonality, so it's confusing to treat them as the same sort of thing.) And
of course, any first-class type would need an associated profile.
Randy.
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 0:22 ` Randy Brukardt
@ 2013-05-11 7:22 ` Yannick Duchêne (Hibou57)
0 siblings, 0 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-11 7:22 UTC (permalink / raw)
Le Sat, 11 May 2013 02:22:58 +0200, Randy Brukardt <randy@rrsoftware.com>
a écrit:
> One of the reasons I chose "profile" for the name of the thingy that I
> was
> describing on top of types was that I expected it to include profile
> operations. That's because I figured that a redesign of Ada would have
> first-class subprogram types; (along with subprogram objects); there is
> no
> good reason to use explicit "access" values for this.
I like the idea (it happened I missed the same with some use case).
> (Object access values
> are so different from the subprogram kind that there is virtually no
> commonality, so it's confusing to treat them as the same sort of thing.)
Sure, unless someone want to allocate executable memory and dynamically
create a sub‑program there in some way (that's feasible at least on Linux
and suggested by POSIX), but that would be a different type of sub‑program
and access anyway.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-09 22:19 ` Randy Brukardt
2013-05-10 3:29 ` Yannick Duchêne (Hibou57)
2013-05-10 3:47 ` Yannick Duchêne (Hibou57)
@ 2013-05-10 3:59 ` Yannick Duchêne (Hibou57)
2013-05-10 4:03 ` Yannick Duchêne (Hibou57)
` (2 subsequent siblings)
5 siblings, 0 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-10 3:59 UTC (permalink / raw)
Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt <randy@rrsoftware.com>
a écrit:
>> 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". :-)
If two subtypes of a same root type can be used interchangeably in some
context, that's nothing justifying weak typing, that's just the rules with
subtypes. Or I miss‑understood the point?
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-09 22:19 ` Randy Brukardt
` (2 preceding siblings ...)
2013-05-10 3:59 ` Yannick Duchêne (Hibou57)
@ 2013-05-10 4:03 ` Yannick Duchêne (Hibou57)
2013-05-10 7:48 ` Dmitry A. Kazakov
2013-05-14 12:46 ` Weaker typing as a part of the way to stronger typing? (Was: Seeking for papers about tagged types vs access to subprograms) Jacob Sparre Andersen
5 siblings, 0 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-10 4:03 UTC (permalink / raw)
Le Fri, 10 May 2013 00:19:14 +0200, Randy Brukardt <randy@rrsoftware.com>
a écrit:
>> 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.
No, and not more than one may defines a new subtypes for the result of
each numeric operations of a program. One may do if he/she wish or sees a
good reason, but that's not required.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-09 22:19 ` Randy Brukardt
` (3 preceding siblings ...)
2013-05-10 4:03 ` Yannick Duchêne (Hibou57)
@ 2013-05-10 7:48 ` Dmitry A. Kazakov
2013-05-10 8:12 ` Yannick Duchêne (Hibou57)
2013-05-11 0:42 ` Randy Brukardt
2013-05-14 12:46 ` Weaker typing as a part of the way to stronger typing? (Was: Seeking for papers about tagged types vs access to subprograms) Jacob Sparre Andersen
5 siblings, 2 replies; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-10 7:48 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-10 7:48 ` Dmitry A. Kazakov
@ 2013-05-10 8:12 ` Yannick Duchêne (Hibou57)
2013-05-10 15:11 ` Yannick Duchêne (Hibou57)
2013-05-11 0:42 ` Randy Brukardt
1 sibling, 1 reply; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-10 8:12 UTC (permalink / raw)
Le Fri, 10 May 2013 09:48:26 +0200, Dmitry A. Kazakov
<mailbox@dmitry-kazakov.de> a écrit:
>> Typing is too rigid to do a good job
>
> Typing is necessarily rigid because
I think he meant something else when he said “rigid”. I understood he
meant “not expressive enough”, “not always applicable”. I would say
“limited” (which is less ambiguous, except in terms of Ada wordings).
> 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.
To be able to apply types beyond trivial cases, would need to have types
beyond trivial types. If it is supposed type must be as they already are,
there is not solution. If it is supposed the concept of type must be
defined, I would say it is what holds a set of axioms which will be
automatically pulled in a context with each reference to that type.
Actually, and except with discriminated records and pre/post condition
(which are not statically checked), the only static capability of types,
is to enumerate a simple list of values and list operations applicable to
that list of values. That's indeed too limited except for trivial cases.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-10 8:12 ` Yannick Duchêne (Hibou57)
@ 2013-05-10 15:11 ` Yannick Duchêne (Hibou57)
0 siblings, 0 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-10 15:11 UTC (permalink / raw)
Le Fri, 10 May 2013 10:12:22 +0200, Yannick Duchêne (Hibou57)
<yannick_duchene@yahoo.fr> a écrit:
> Actually, and except with discriminated records and pre/post condition
> (which are not statically checked), the only static capability of types,
> is to enumerate a simple list of values and list operations applicable
> to that list of values. That's indeed too limited except for trivial
> cases.
I was wrong, forgetting an important one: Ada types can be described by
their origins too. I mean the thing you get when you tell a type has only
a private full definition and have functions returning an instance of that
type. These functions are the origin of instances, and more or less
express what instances are, as the assertions about what's returned by the
function, finally becomes assertions of the type. These functions are
finally part of the type definition too. That's informal specifications,
while that still opens the door to better.
That's a consequence of type being matched by name and not by structure
(that's a reason why type matched by name is better, more expressive).
As a summary of what's available to describe a type:
* list of contiguous values (unfortunately, holes are not allowed,
except using static predicates);
* list of applicable operations (unfortunately, very poorly specified:
only signature);
* invariant predicate (unfortunately, not statically checked, except
with static predicate);
* functions generating the initial values (for private types only, not
trustable otherwise).
(did I still forget one?)
Not enough, while finally not that bad.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-10 7:48 ` Dmitry A. Kazakov
2013-05-10 8:12 ` Yannick Duchêne (Hibou57)
@ 2013-05-11 0:42 ` Randy Brukardt
2013-05-11 6:37 ` Dmitry A. Kazakov
` (2 more replies)
1 sibling, 3 replies; 202+ messages in thread
From: Randy Brukardt @ 2013-05-11 0:42 UTC (permalink / raw)
"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.
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 0:42 ` Randy Brukardt
@ 2013-05-11 6:37 ` Dmitry A. Kazakov
2013-05-11 7:06 ` Georg Bauhaus
` (2 more replies)
2013-05-11 7:32 ` Yannick Duchêne (Hibou57)
2013-05-11 7:46 ` Yannick Duchêne (Hibou57)
2 siblings, 3 replies; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-11 6:37 UTC (permalink / raw)
On Fri, 10 May 2013 19:42:37 -0500, Randy Brukardt wrote:
> "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.
That applies to stateful types only. Not every type is stateful. Bringing
state into objects is considered bad practice. So bad, that it motivated
some people to invent whole programming paradigms to avoid stateful object,
e.g. functional programming. The sole idea of FP is to sweep states under
the carpet.
Stateful OOA/D vs. stateless FP are both extremes, but in any case one
should not base the language design (!) on exposing states. State machines
existed since the beginning of computing. As a compiler designer you should
know better how difficult, almost impossibly, it is to use state machine
patterns.
>>> 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.
On top of something which formalization of you call madness?
>>>> 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.
Dynamically? Because if statically, then that is exactly what is called a
type. When dynamically, why bother yourself inventing another SmallTalk? It
is already there.
> 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.
First of all, there are preconditions of operations and the precondition
put on individual calls. I don't know which one you mean here. But the
preconditions of operations must be statically true. Meaning: a declared
operation can be called anywhere. The client may annotate his calls to the
operation with additional preconditions related to the logic of the program
that uses the operation. These are not the property of the operation and
unrelated to the type.
The idea that the precondition of first kind should depend on the state of
the objects involved in the operation is a very, VERY bad idea.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 6:37 ` Dmitry A. Kazakov
@ 2013-05-11 7:06 ` Georg Bauhaus
2013-05-11 7:42 ` Dmitry A. Kazakov
2013-05-11 7:58 ` Yannick Duchêne (Hibou57)
2013-05-11 8:03 ` Yannick Duchêne (Hibou57)
2 siblings, 1 reply; 202+ messages in thread
From: Georg Bauhaus @ 2013-05-11 7:06 UTC (permalink / raw)
On 11.05.13 08:37, Dmitry A. Kazakov wrote:
> First of all, there are preconditions of operations and the precondition
> put on individual calls. I don't know which one you mean here. But the
> preconditions of operations must be statically true. Meaning: a declared
> operation can be called anywhere. The client may annotate his calls to the
> operation with additional preconditions related to the logic of the program
> that uses the operation. These are not the property of the operation and
> unrelated to the type.
>
> The idea that the precondition of first kind should depend on the state of
> the objects involved in the operation is a very, VERY bad idea.
How do you specify the preconditions of the second kind (on individual
calls) in such a way that a programmer, wishing to calling these operations,
ensures the calls won't fail as a consequence of violating these
preconditions?
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 7:06 ` Georg Bauhaus
@ 2013-05-11 7:42 ` Dmitry A. Kazakov
2013-05-11 8:14 ` Yannick Duchêne (Hibou57)
2013-05-14 2:29 ` Randy Brukardt
0 siblings, 2 replies; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-11 7:42 UTC (permalink / raw)
On Sat, 11 May 2013 09:06:11 +0200, Georg Bauhaus wrote:
> On 11.05.13 08:37, Dmitry A. Kazakov wrote:
>> First of all, there are preconditions of operations and the precondition
>> put on individual calls. I don't know which one you mean here. But the
>> preconditions of operations must be statically true. Meaning: a declared
>> operation can be called anywhere. The client may annotate his calls to the
>> operation with additional preconditions related to the logic of the program
>> that uses the operation. These are not the property of the operation and
>> unrelated to the type.
>>
>> The idea that the precondition of first kind should depend on the state of
>> the objects involved in the operation is a very, VERY bad idea.
>
> How do you specify the preconditions of the second kind (on individual
> calls) in such a way that a programmer, wishing to calling these operations,
> ensures the calls won't fail as a consequence of violating these
> preconditions?
"Fail" is a wrong word here. The right wording is ensuring postconditions.
That is completely unrelated issue, IMO.
I have a feeling that people confuse typing with this, which is basically
program correctness en large. You cannot ensure program correctness through
types. And since full correctness proof is unachievable anyway I want to
separate it from types.
Second kind checks (e.g. SPARK) should be optional so that the programmer
would add or remove checks depending on requirements and provability.
Especially because there is also a big difference in the design of type
checks and correctness checks. We design types top-down, at least the most
important ones. Type design is frequently irreversible, few things can be
changed later without big troubles. It is almost waterfall. On the
contrary, the correctness checks are bottom-up. You probably never get to
the top. But you can well figure up essential things at the bottom for
which it were possible and desirable to check things statically.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 7:42 ` Dmitry A. Kazakov
@ 2013-05-11 8:14 ` Yannick Duchêne (Hibou57)
2013-05-14 2:29 ` Randy Brukardt
1 sibling, 0 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-11 8:14 UTC (permalink / raw)
Le Sat, 11 May 2013 09:42:14 +0200, Dmitry A. Kazakov
<mailbox@dmitry-kazakov.de> a écrit:
> "Fail" is a wrong word here. The right wording is ensuring
> postconditions.
> That is completely unrelated issue, IMO.
>
> I have a feeling that people confuse typing with this, which is basically
> program correctness en large. You cannot ensure program correctness
> through
> types. And since full correctness proof is unachievable anyway I want to
> separate it from types.
>
> Second kind checks (e.g. SPARK) should be optional so that the programmer
> would add or remove checks depending on requirements and provability.
>
> Especially because there is also a big difference in the design of type
> checks and correctness checks. We design types top-down, at least the
> most
> important ones. Type design is frequently irreversible, few things can be
> changed later without big troubles. It is almost waterfall. On the
> contrary, the correctness checks are bottom-up. You probably never get to
> the top. But you can well figure up essential things at the bottom for
> which it were possible and desirable to check things statically.
All sounds wise to me, agree.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 7:42 ` Dmitry A. Kazakov
2013-05-11 8:14 ` Yannick Duchêne (Hibou57)
@ 2013-05-14 2:29 ` Randy Brukardt
2013-05-14 7:44 ` Dmitry A. Kazakov
1 sibling, 1 reply; 202+ messages in thread
From: Randy Brukardt @ 2013-05-14 2:29 UTC (permalink / raw)
"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
news:hxkln519n179.1kt13z7phxg2f.dlg@40tude.net...
> On Sat, 11 May 2013 09:06:11 +0200, Georg Bauhaus wrote:
>
>> On 11.05.13 08:37, Dmitry A. Kazakov wrote:
>>> First of all, there are preconditions of operations and the precondition
>>> put on individual calls. I don't know which one you mean here. But the
>>> preconditions of operations must be statically true. Meaning: a declared
>>> operation can be called anywhere. The client may annotate his calls to
>>> the
>>> operation with additional preconditions related to the logic of the
>>> program
>>> that uses the operation. These are not the property of the operation and
>>> unrelated to the type.
>>>
>>> The idea that the precondition of first kind should depend on the state
>>> of
>>> the objects involved in the operation is a very, VERY bad idea.
>>
>> How do you specify the preconditions of the second kind (on individual
>> calls) in such a way that a programmer, wishing to calling these
>> operations,
>> ensures the calls won't fail as a consequence of violating these
>> preconditions?
>
> "Fail" is a wrong word here. The right wording is ensuring postconditions.
> That is completely unrelated issue, IMO.
>
> I have a feeling that people confuse typing with this, which is basically
> program correctness en large. You cannot ensure program correctness
> through
> types. And since full correctness proof is unachievable anyway I want to
> separate it from types.
>
> Second kind checks (e.g. SPARK) should be optional so that the programmer
> would add or remove checks depending on requirements and provability.
Which is why I'm suggesting something built on top of Ada's types for this
purpose.
> Especially because there is also a big difference in the design of type
> checks and correctness checks. We design types top-down, at least the most
> important ones. Type design is frequently irreversible, few things can be
> changed later without big troubles. It is almost waterfall. On the
> contrary, the correctness checks are bottom-up. You probably never get to
> the top. But you can well figure up essential things at the bottom for
> which it were possible and desirable to check things statically.
Again, this is precisely what I'm talking about. SPARK is a disaster because
it insists that you do everything it's way, or nothing at all. I want to be
able to incrementally add checks as they become apparent.
The big disconnect is that you (and lots of other misguided people) think
that types have something to do with operations. Types are more fundamental
than operations; they get *used* in operations, rather than the operations
being part of the type. Ideally, a type is nothing but a black box (an Ada
private type). Operations are the next level of complexity, and exist
separately from the types.
Randy.
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-14 2:29 ` Randy Brukardt
@ 2013-05-14 7:44 ` Dmitry A. Kazakov
2013-05-14 11:34 ` Yannick Duchêne (Hibou57)
0 siblings, 1 reply; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-14 7:44 UTC (permalink / raw)
On Mon, 13 May 2013 21:29:15 -0500, Randy Brukardt wrote:
> The big disconnect is that you (and lots of other misguided people) think
> that types have something to do with operations. Types are more fundamental
> than operations; they get *used* in operations, rather than the operations
> being part of the type.
Neither type nor operation nor value exist before other. You cannot
separate them. It is like magnetic field and current.
> Operations are the next level of complexity, and exist
> separately from the types.
You cannot define operation without type and conversely. Your concept comes
from languages of 60's built upon predefined types, e.g. FORTRAN. There
predefined types were given and the rest only used them as building blocks
for algorithms.
The point is that conceptually there is nothing special in such types. They
are not better (no more fundamental) and not worse than user-defined types.
And the operations you define on them are as much operations as the
built-in operations. Operations and types are fully equal.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-14 7:44 ` Dmitry A. Kazakov
@ 2013-05-14 11:34 ` Yannick Duchêne (Hibou57)
2013-05-14 12:16 ` Dmitry A. Kazakov
0 siblings, 1 reply; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-14 11:34 UTC (permalink / raw)
Le Tue, 14 May 2013 09:44:00 +0200, Dmitry A. Kazakov
<mailbox@dmitry-kazakov.de> a écrit:
> On Mon, 13 May 2013 21:29:15 -0500, Randy Brukardt wrote:
>
>> The big disconnect is that you (and lots of other misguided people)
>> think
>> that types have something to do with operations. Types are more
>> fundamental
>> than operations; they get *used* in operations, rather than the
>> operations
>> being part of the type.
>
> Neither type nor operation nor value exist before other. You cannot
> separate them. It is like magnetic field and current.
An operation has a type, while a type may be defined without operations
(not a lot useful, however still possible). The type gets realised even
before runtime (except for some subtypes), most values too, while an
operation, is nothing but a value (with an implicit type) before runtime.
Values and types, seems to me the most fundamental concept. At least, this
looks unavoidable for analysis, which looks at everything, as if it was
static.
If a program is mainly a structure, then it is mainly made of typed values
(and the program as a whole, is a complex value). Functional programming,
where even a function is a value, won't say the opposite.
This fact is also what makes the differences between data (hopefully typed
data) and program, narrow, and a matter of interpretation (not that much
apparent with general purpose languages such as Ada; more apparent with
domain‑specific‑languages).
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-14 11:34 ` Yannick Duchêne (Hibou57)
@ 2013-05-14 12:16 ` Dmitry A. Kazakov
2013-05-14 13:13 ` Yannick Duchêne (Hibou57)
` (2 more replies)
0 siblings, 3 replies; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-14 12:16 UTC (permalink / raw)
On Tue, 14 May 2013 13:34:09 +0200, Yannick Duchêne (Hibou57) wrote:
> Le Tue, 14 May 2013 09:44:00 +0200, Dmitry A. Kazakov
> <mailbox@dmitry-kazakov.de> a écrit:
>
>> Neither type nor operation nor value exist before other. You cannot
>> separate them. It is like magnetic field and current.
>
> An operation has a type,, while a type may be defined without operations
> (not a lot useful, however still possible).
procedure Foo;
> If a program is mainly a structure, then it is mainly made of typed values
> (and the program as a whole, is a complex value).
No idea, what does this mean.
Value is not a programming language term, it belongs to the application
domain. Value is the meaning attributed to the state of a typed object in
some context.
E.g.
Salary : Buckazoid := 1;
Salary is meant to have the value of 1 Buckazoid.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-14 12:16 ` Dmitry A. Kazakov
@ 2013-05-14 13:13 ` Yannick Duchêne (Hibou57)
2013-05-14 18:41 ` Randy Brukardt
2013-05-15 11:20 ` Peter C. Chapin
2 siblings, 0 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-14 13:13 UTC (permalink / raw)
Le Tue, 14 May 2013 14:16:52 +0200, Dmitry A. Kazakov
<mailbox@dmitry-kazakov.de> a écrit:
> On Tue, 14 May 2013 13:34:09 +0200, Yannick Duchêne (Hibou57) wrote:
>> An operation has a type,, while a type may be defined without operations
>> (not a lot useful, however still possible).
>
> procedure Foo;
This is not random data, this has type. The type is implicit in most case
and becomes more explicit with access to sub‑program (the same with many
other languages), and as well‑known, there is nothing in Ada looking like
an access to an untyped entity, which implies the sub‑program has an
implicit type. You just can't dynamically create or manipulate value of
that type in Ada (unlike with say, SML or other LISP variant), which makes
that type special, and prevented it to be given a name, a syntax or ever
be explicitly referred to in Ada (not the same with all languages).
>> If a program is mainly a structure, then it is mainly made of typed
>> values
>> (and the program as a whole, is a complex value).
>
> No idea, what does this mean.
>
> Value is not a programming language term, it belongs to the application
> domain.
Then think about meta‑programming or “programming as a human activity”.
That said, obviously, the concept of value I referred to, was either at a
level higher than values manipulated by the program, or else, constants
values referred to (and interpreted) by the program.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-14 12:16 ` Dmitry A. Kazakov
2013-05-14 13:13 ` Yannick Duchêne (Hibou57)
@ 2013-05-14 18:41 ` Randy Brukardt
2013-05-15 11:20 ` Peter C. Chapin
2 siblings, 0 replies; 202+ messages in thread
From: Randy Brukardt @ 2013-05-14 18:41 UTC (permalink / raw)
"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
news:mk9m6fxa1jbr$.mm0kw7g3igma$.dlg@40tude.net...
...
> Value is not a programming language term, it belongs to the application
> domain.
The Ada Standard uses the word an awful lot (starting with 3.2(1)) for
something that isn't "a programming language term". The AARM even gives a
definition for "value" (3.2(10.a)). I'd say that it certainly is a
programming language term, but it's one whose meaning is assumed to be
understood and thus is axiomatic. (There are of course a number of such
terms, it would be impossible to define every word used in a Standard.)
Randy.
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-14 12:16 ` Dmitry A. Kazakov
2013-05-14 13:13 ` Yannick Duchêne (Hibou57)
2013-05-14 18:41 ` Randy Brukardt
@ 2013-05-15 11:20 ` Peter C. Chapin
2013-05-15 13:00 ` Dmitry A. Kazakov
2 siblings, 1 reply; 202+ messages in thread
From: Peter C. Chapin @ 2013-05-15 11:20 UTC (permalink / raw)
On Tue, 14 May 2013, Dmitry A. Kazakov wrote:
> procedure Foo;
This procedure does nothing unless it has side effects. If so, then those
side effects entail operations on values of a particular type.
> Value is not a programming language term, it belongs to the application
> domain. Value is the meaning attributed to the state of a typed object in
> some context.
>
> E.g.
>
> Salary : Buckazoid := 1;
>
> Salary is meant to have the value of 1 Buckazoid.
A type is a pair of sets: a set of values and a set of operations defined
over those values (for example as functions taking items from the first
set as a parameter). Either set can be empty. In any case "value" is most
certainly a programming language term. You can't talk about a type without
talking about the values that inhabit that type (again, could be an empty
set in certain special cases).
Peter
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-15 11:20 ` Peter C. Chapin
@ 2013-05-15 13:00 ` Dmitry A. Kazakov
2013-05-15 21:12 ` Peter C. Chapin
0 siblings, 1 reply; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-15 13:00 UTC (permalink / raw)
On Wed, 15 May 2013 07:20:23 -0400, Peter C. Chapin wrote:
> On Tue, 14 May 2013, Dmitry A. Kazakov wrote:
>
>> procedure Foo;
>
> This procedure does nothing unless it has side effects. If so, then those
> side effects entail operations on values of a particular type.
Nevertheless it is an operation that does not refer to any particular type.
>> Value is not a programming language term, it belongs to the application
>> domain. Value is the meaning attributed to the state of a typed object in
>> some context.
>>
>> E.g.
>>
>> Salary : Buckazoid := 1;
>>
>> Salary is meant to have the value of 1 Buckazoid.
>
> A type is a pair of sets: a set of values and a set of operations defined
> over those values (for example as functions taking items from the first
> set as a parameter). Either set can be empty. In any case "value" is most
> certainly a programming language term.
type Employee is ...;
How is employee a language term?
task type Driver is ...;
Show me an RM section which defines the values of this type.
And the simplest possible example why the language has nothing to do with
values is this:
type Some_Transcendental_Numbers is (e, Pi, Euler);
What is the value of e?
> You can't talk about a type without
> talking about the values that inhabit that type (again, could be an empty
> set in certain special cases).
This is what I said in response to Randy. That type, operations, values
cannot be separated to each other. Neither is more or less fundamental than
other.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-15 13:00 ` Dmitry A. Kazakov
@ 2013-05-15 21:12 ` Peter C. Chapin
2013-05-15 22:08 ` Dmitry A. Kazakov
0 siblings, 1 reply; 202+ messages in thread
From: Peter C. Chapin @ 2013-05-15 21:12 UTC (permalink / raw)
On Wed, 15 May 2013, Dmitry A. Kazakov wrote:
>>> procedure Foo;
>>
>> This procedure does nothing unless it has side effects. If so, then those
>> side effects entail operations on values of a particular type.
>
> Nevertheless it is an operation that does not refer to any particular type.
It doesn't refer to the type in the source text because of the limitations
of the Ada language (specifically, side effects remain undocumented).
SPARK rectifies that to some degree with global annotations. However, the
operation is still an operation on values of some type.
>> A type is a pair of sets: a set of values and a set of operations defined
>> over those values (for example as functions taking items from the first
>> set as a parameter). Either set can be empty. In any case "value" is most
>> certainly a programming language term.
>
> type Employee is ...;
>
> How is employee a language term?
Weren't we talking about "value" as a programming language term? I
understand that to mean "value" as something used by people when talking
about programming languages. "Employees" is just a name in some program...
and specifically the name of a type. I don't follow what this has to do
with a discussion about values.
> task type Driver is ...;
>
> Show me an RM section which defines the values of this type.
The values of a task type are the code fragments that implement the
task. Here I'm speaking in general terms, of course.
> And the simplest possible example why the language has nothing to do with
> values is this:
>
> type Some_Transcendental_Numbers is (e, Pi, Euler);
>
> What is the value of e?
Some_Transcendental_Numbers is an enumeration type. One of it's values is
'e'. There is no significance to 'e' other than that. At least at the
level of types.
Peter
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-15 21:12 ` Peter C. Chapin
@ 2013-05-15 22:08 ` Dmitry A. Kazakov
2013-05-16 11:31 ` Peter C. Chapin
0 siblings, 1 reply; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-15 22:08 UTC (permalink / raw)
On Wed, 15 May 2013 17:12:09 -0400, Peter C. Chapin wrote:
> On Wed, 15 May 2013, Dmitry A. Kazakov wrote:
>
>>> A type is a pair of sets: a set of values and a set of operations defined
>>> over those values (for example as functions taking items from the first
>>> set as a parameter). Either set can be empty. In any case "value" is most
>>> certainly a programming language term.
>>
>> type Employee is ...;
>>
>> How is employee a language term?
>
> Weren't we talking about "value" as a programming language term?
You consider value being a language term. I objected, pointing out that
value is the meaning of some program state, the meaning which is always
outside the language and from the problem space. The only case when a value
can be an Ada term is when the program is an Ada compiler.
> I
> understand that to mean "value" as something used by people when talking
> about programming languages.
Yes.
> "Employees" is just a name in some program...
> and specifically the name of a type. I don't follow what this has to do
> with a discussion about values.
The type Employee has values denoting employees of some business in some
Ada program.
>> task type Driver is ...;
>>
>> Show me an RM section which defines the values of this type.
>
> The values of a task type are the code fragments that implement the
> task. Here I'm speaking in general terms, of course.
So,
X, Y : Driver;
have same values? You seem to confuse value for its representation. The
value of a task type is not even computable, or the value of clock. The
representation of a task value might be a combination of some code, TCB,
the state of system queues etc.
>> And the simplest possible example why the language has nothing to do with
>> values is this:
>>
>> type Some_Transcendental_Numbers is (e, Pi, Euler);
>>
>> What is the value of e?
>
> Some_Transcendental_Numbers is an enumeration type. One of it's values is
> 'e'. There is no significance to 'e' other than that. At least at the
> level of types.
And what significance has Ada.Numerics'
e : constant :=
2.71828_18284_59045_23536_02874_71352_66249_77572_47093_69996;
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-15 22:08 ` Dmitry A. Kazakov
@ 2013-05-16 11:31 ` Peter C. Chapin
2013-05-16 11:56 ` Yannick Duchêne (Hibou57)
` (2 more replies)
0 siblings, 3 replies; 202+ messages in thread
From: Peter C. Chapin @ 2013-05-16 11:31 UTC (permalink / raw)
On Thu, 16 May 2013, Dmitry A. Kazakov wrote:
>> Weren't we talking about "value" as a programming language term?
>
> You consider value being a language term. I objected, pointing out that
> value is the meaning of some program state, the meaning which is always
> outside the language and from the problem space. The only case when a
> value can be an Ada term is when the program is an Ada compiler.
>
>> I understand that to mean "value" as something used by people when
>> talking about programming languages.
>
> Yes.
You said earlier, "value is the meaning of some program state..." So
"value" is, indeed, a term used when discussing programming languages.
That was my original contention. Recall that we were talking about types
and values and their relationship. I again return to my original
statement: a type is two sets, a set of values and a set of operations.
Are you disagreeing with that? I honestly can't tell.
> So,
>
> X, Y : Driver;
>
> have same values?
Yes, I would say so.
> You seem to confuse value for its representation. The value of a task
> type is not even computable, or the value of clock. The representation
> of a task value might be a combination of some code, TCB, the state of
> system queues etc.
I actually don't think I'm all that confused. I borrow concepts that are
standard in functional languages where functions are, indeed, first class
values. There a function's value is its (source) code. Two different
instances of the same function represent the same value just as two
different instances of the integer literal "2" represent the same value.
The machine representation of a function---how it is converted to
executable form---is at the compiler's discretion, of course. In some
languages function types have only a single operation, that of
"application" (calling). Some of the items you mentioned above exist to
support the execution of that operation; they are not part of the value.
Ada tasks are not quite like functions but conceptually there are
similarities. One important limitation of Ada is that every task type is
inhabited with only a single value. It isn't possible to create multiple
task bodies behind a task type definition. In contrast consider:
function F1(X : Integer) return String;
function F2(X : Integer) return String;
Here F1 and F2 have the same "function type." They are two different
values that inhabit that type just as "2" and "3" are two different values
inhabiting Integer.
But if you say
task type T is
...
end T;
You can only write one body to go with the type. Every instance of type T
thus has the same value---the type has only one value.
This limitation doesn't change the concepts, it just reflects a limitation
of Ada. In the more general case there would be "task operators" that
would allow you to compose tasks to make new tasks (higher order tasks?)
and you would be able to store different tasks into the same variable of
task type provided all the tasks had the same type (but possibly different
bodies). Of course this language isn't Ada.
That said, the Ada 2005 features of synchronized and protected interfaces
are moving into this terrian. A full theoretical accounting of Ada task
types would be a very interesting exercise (has it been done?).
> And what significance has Ada.Numerics'
>
> e : constant :=
> 2.71828_18284_59045_23536_02874_71352_66249_77572_47093_69996;
As I understand it, 'e' has type Universal_Float and the 2.718... is a
value inhabiting that type. I guess I don't understand what point you are
making here. I apologize if I cut too much context.
Peter
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-16 11:31 ` Peter C. Chapin
@ 2013-05-16 11:56 ` Yannick Duchêne (Hibou57)
2013-05-16 12:20 ` Dmitry A. Kazakov
2013-05-16 13:09 ` Eryndlia Mavourneen
2 siblings, 0 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-16 11:56 UTC (permalink / raw)
Le Thu, 16 May 2013 13:31:58 +0200, Peter C. Chapin <PChapin@vtc.vsc.edu>
a écrit:
> I again return to my original statement: a type is two sets, a set of
> values and a set of operations.
There is nothing like operation as something distinct from values, at
least formally. Operations as understood in procedural languages, is an
interpretation, especially when it has side effects, it differs entirely.
There is no operations, and there are at most functions, which are
expressions which are values (a partially evaluated expression like a
function is supposed to be most often unless constant, is still a value,
this is just a set which is that of a domain, still a value).
(don't kick too hard if it happens I'm boring :D )
I feel there is a mix of formal definitions and language specific
definitions, while both can't be mixed.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-16 11:31 ` Peter C. Chapin
2013-05-16 11:56 ` Yannick Duchêne (Hibou57)
@ 2013-05-16 12:20 ` Dmitry A. Kazakov
2013-05-16 13:10 ` Peter C. Chapin
2013-05-16 13:09 ` Eryndlia Mavourneen
2 siblings, 1 reply; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-16 12:20 UTC (permalink / raw)
On Thu, 16 May 2013 07:31:58 -0400, Peter C. Chapin wrote:
> On Thu, 16 May 2013, Dmitry A. Kazakov wrote:
>
>>> Weren't we talking about "value" as a programming language term?
>>
>> You consider value being a language term. I objected, pointing out that
>> value is the meaning of some program state, the meaning which is always
>> outside the language and from the problem space. The only case when a
>> value can be an Ada term is when the program is an Ada compiler.
>>
>>> I understand that to mean "value" as something used by people when
>>> talking about programming languages.
>>
>> Yes.
>
> You said earlier, "value is the meaning of some program state..." So
> "value" is, indeed, a term used when discussing programming languages.
> That was my original contention. Recall that we were talking about types
> and values and their relationship. I again return to my original
> statement: a type is two sets, a set of values and a set of operations.
> Are you disagreeing with that?
No. Why should I?
>> So,
>>
>> X, Y : Driver;
>>
>> have same values?
>
> Yes, I would say so.
Really? X is an *equivalent* of Y?
>> You seem to confuse value for its representation. The value of a task
>> type is not even computable, or the value of clock. The representation
>> of a task value might be a combination of some code, TCB, the state of
>> system queues etc.
>
> I actually don't think I'm all that confused. I borrow concepts that are
> standard in functional languages where functions are, indeed, first class
> values. There a function's value is its (source) code. Two different
> instances of the same function represent the same value just as two
> different instances of the integer literal "2" represent the same value.
Because the literal 2 [of type Integer] denotes the same value in all
contexts. But X, Y : Driver clearly do not do that. If X and Y are not
equivalent how they could have the same value? Either the values are
different or else you need to bring some other stuff beyond types, values
and operations into the picture.
>> And what significance has Ada.Numerics'
>>
>> e : constant :=
>> 2.71828_18284_59045_23536_02874_71352_66249_77572_47093_69996;
>
> As I understand it, 'e' has type Universal_Float and the 2.718... is a
> value inhabiting that type. I guess I don't understand what point you are
> making here.
The point is about the value of e. You said that when declared as I did, it
has no significance, just a random pattern of bits. Do I interpret you
correctly? Does this same logic apply to e of Ada.Numerics? If not where is
a difference? If you think that values should have "significance", then
what is significance? Why enumeration value does not have it and
Universal_Integer does?
P.S. What you call "significance" is the value. What you call "value" is a
representation.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-16 12:20 ` Dmitry A. Kazakov
@ 2013-05-16 13:10 ` Peter C. Chapin
2013-05-16 13:54 ` Dmitry A. Kazakov
0 siblings, 1 reply; 202+ messages in thread
From: Peter C. Chapin @ 2013-05-16 13:10 UTC (permalink / raw)
On Thu, 16 May 2013, Dmitry A. Kazakov wrote:
>>> So,
>>>
>>> X, Y : Driver;
>>>
>>> have same values?
>>
>> Yes, I would say so.
>
> Really? X is an *equivalent* of Y?
Sure. If it were allowed the expression 'X = Y' should return True. I
realize that equivalence of functions is a difficult concept in general (I
believe it's undecidable to determine if two functions f_1 and f_2 are
equivalent even if you can see the source code of both) but here since the
code for both X and Y is, in fact, the very same program text, it seems
clear that they are equivalent.
X and Y above of course may contain different state information as they
run but that's all related to the operation of execution; it doesn't
distinguish their "task values."
These concepts are all quite straightforward, it seems to me, in the
context of functional languages. Of course Ada isn't a functional language
and it has side effects, etc, so things do get a bit messier. I still
contend, however, that the basic ideas still... er... apply.
> Because the literal 2 [of type Integer] denotes the same value in all
> contexts. But X, Y : Driver clearly do not do that. If X and Y are not
> equivalent how they could have the same value?
I guess this is where we disagree. To me X and Y do denote the same value
in all contexts; they are equivalent.
> Either the values are different or else you need to bring some other
> stuff beyond types, values and operations into the picture.
Are you referring to the execution state here? To my mind that dynamic
information is just part of the operation of execution. It's necessary to
make that operation work but, yes, I agree that it is a separate matter
from the types and values, etc.
Modeling state in a clean way is slippery business. You might be able to
bring it into the context of this discussion by treating the state of each
task as a kind of mutable parameter to the task. As such there could be an
implicit type for that parameter... some kind of record type, etc... but
it does get messy.
>>> e : constant :=
>>> 2.71828_18284_59045_23536_02874_71352_66249_77572_47093_69996;
>>
>> As I understand it, 'e' has type Universal_Float and the 2.718... is a
>> value inhabiting that type. I guess I don't understand what point you are
>> making here.
>
> The point is about the value of e. You said that when declared as I did, it
> has no significance, just a random pattern of bits. Do I interpret you
> correctly? Does this same logic apply to e of Ada.Numerics? If not where is
> a difference?
We're talking about two different 'e's here. In the first case 'e' was an
enumeration literal. The type in that example was suggestively named
Transcendental_Constants (or something like that... I forget exactly), but
any connection between 'e' and the mathematical value of e was purely in
the mind of the programmer. In Ada terms 'e' was a value of that type but
nothing beyond that. That's what I meant by it not having any
significance.
In the second case 'e' is a named number bound to a value in the
Universal_Float type that is clearly intended to be the mathematical e...
at least to the closest degree permitted by the available values in that
type (I guess in this case it's really limited by the amount of space the
implementer wants to use when writing the declaration. Am I correct in
saying that Universal_Float has infinite precision?)
I suppose I don't understand the point you were trying to make originally
with the enumeration type. There 'e' was a value of the specified type.
Was that it?
Peter
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-16 13:10 ` Peter C. Chapin
@ 2013-05-16 13:54 ` Dmitry A. Kazakov
2013-05-16 17:15 ` G.B.
0 siblings, 1 reply; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-16 13:54 UTC (permalink / raw)
On Thu, 16 May 2013 09:10:11 -0400, Peter C. Chapin wrote:
> On Thu, 16 May 2013, Dmitry A. Kazakov wrote:
>
>>>> So,
>>>>
>>>> X, Y : Driver;
>>>>
>>>> have same values?
>>>
>>> Yes, I would say so.
>>
>> Really? X is an *equivalent* of Y?
>
> Sure. If it were allowed the expression 'X = Y' should return True.
If X嚙踝蕭Y, you don't need two instances of.
> I realize that equivalence of functions is a difficult concept in general
There is nothing difficult in that. A function is a set of pairs. Two sets
are equal when contain same elements.
> X and Y above of course may contain different state information as they
> run but that's all related to the operation of execution; it doesn't
> distinguish their "task values."
Of course it does. For example: it can happen that X'Terminated /=
Y'Terminated.
>> Because the literal 2 [of type Integer] denotes the same value in all
>> contexts. But X, Y : Driver clearly do not do that. If X and Y are not
>> equivalent how they could have the same value?
>
> I guess this is where we disagree. To me X and Y do denote the same value
> in all contexts; they are equivalent.
They are evidently not, which can be easily demonstrated by presenting a
program which would yield different results depending on whether X or Y is
used.
>> Either the values are different or else you need to bring some other
>> stuff beyond types, values and operations into the picture.
>
> Are you referring to the execution state here?
It is your concept, I am only giving you enough rope to hang yourselves...
> To my mind that dynamic
> information is just part of the operation of execution. It's necessary to
> make that operation work but, yes, I agree that it is a separate matter
> from the types and values, etc.
Which means that your model is inadequate to describe the way programs
work, and more generally to programming.
>>>> e : constant :=
>>>> 2.71828_18284_59045_23536_02874_71352_66249_77572_47093_69996;
>>>
>>> As I understand it, 'e' has type Universal_Float and the 2.718... is a
>>> value inhabiting that type. I guess I don't understand what point you are
>>> making here.
>>
>> The point is about the value of e. You said that when declared as I did, it
>> has no significance, just a random pattern of bits. Do I interpret you
>> correctly? Does this same logic apply to e of Ada.Numerics? If not where is
>> a difference?
>
> We're talking about two different 'e's here. In the first case 'e' was an
> enumeration literal. The type in that example was suggestively named
> Transcendental_Constants (or something like that... I forget exactly), but
> any connection between 'e' and the mathematical value of e was purely in
> the mind of the programmer.
How Universal_Integer is different?
> In Ada terms 'e' was a value of that type but
> nothing beyond that. That's what I meant by it not having any
> significance.
>
> In the second case 'e' is a named number bound to a value in the
> Universal_Float type that is clearly intended to be the mathematical e...
How it is more "clearly intended" than enumeration 'e'?
Note that neither is mathematical e. They *model* e = as you said "purely
in the mind of the programmer." This is what value is, an idea behind a
computational state.
> at least to the closest degree permitted by the available values in that
> type (I guess in this case it's really limited by the amount of space the
> implementer wants to use when writing the declaration. Am I correct in
> saying that Universal_Float has infinite precision?)
It has an indefinite precision.
> I suppose I don't understand the point you were trying to make originally
> with the enumeration type. There 'e' was a value of the specified type.
> Was that it?
The value of e was meant to represent the transcendental number e. The type
was meant to model real numbers. Similarly Ada.Numerics e is meant to
represent e. And Universal_Real is meant to model real numbers. e is not
Ada term. It is a term of mathematical analysis. Neither type is real, they
are only models of.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-16 13:54 ` Dmitry A. Kazakov
@ 2013-05-16 17:15 ` G.B.
2013-05-16 18:09 ` Peter C. Chapin
0 siblings, 1 reply; 202+ messages in thread
From: G.B. @ 2013-05-16 17:15 UTC (permalink / raw)
On 16.05.13 15:54, Dmitry A. Kazakov wrote:
>> I realize that equivalence of functions is a difficult concept in general
> There is nothing difficult in that. A function is a set of pairs. Two sets
> are equal when contain same elements.
I think the difficulty is that eq is not computable. For example,
if f1 and f2 are any Ada compilers, produce an algorithm that computes
eq(f1, f2)
Then, proceed to finding eq of procedures computing eq.
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-16 17:15 ` G.B.
@ 2013-05-16 18:09 ` Peter C. Chapin
2013-05-16 19:16 ` Dmitry A. Kazakov
2013-05-16 21:20 ` Niklas Holsti
0 siblings, 2 replies; 202+ messages in thread
From: Peter C. Chapin @ 2013-05-16 18:09 UTC (permalink / raw)
On Thu, 16 May 2013, G.B. wrote:
> On 16.05.13 15:54, Dmitry A. Kazakov wrote:
>>> I realize that equivalence of functions is a difficult concept in general
>> There is nothing difficult in that. A function is a set of pairs. Two sets
>> are equal when contain same elements.
>
> I think the difficulty is that eq is not computable. For example,
> if f1 and f2 are any Ada compilers, produce an algorithm that computes
>
> eq(f1, f2)
>
> Then, proceed to finding eq of procedures computing eq.
The other problem with Dmitry's earlier suggestion is that the sets he's
talking about could be infinite in size (at least in principle). Comparing
infinite sets can't be done in finite time, of course, so it doesn't
really solve the problem in the general case. This is part of being not
computable. I believe computing the equivalence of functions is
undecidable, but I don't have a proof off hand (maybe one could be looked
up).
Peter
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-16 18:09 ` Peter C. Chapin
@ 2013-05-16 19:16 ` Dmitry A. Kazakov
2013-05-16 21:59 ` Georg Bauhaus
2013-05-16 21:20 ` Niklas Holsti
1 sibling, 1 reply; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-16 19:16 UTC (permalink / raw)
On Thu, 16 May 2013 14:09:59 -0400, Peter C. Chapin wrote:
> On Thu, 16 May 2013, G.B. wrote:
>
>> On 16.05.13 15:54, Dmitry A. Kazakov wrote:
>
>>>> I realize that equivalence of functions is a difficult concept in general
>>> There is nothing difficult in that. A function is a set of pairs. Two sets
>>> are equal when contain same elements.
>>
>> I think the difficulty is that eq is not computable. For example,
>> if f1 and f2 are any Ada compilers, produce an algorithm that computes
>>
>> eq(f1, f2)
>>
>> Then, proceed to finding eq of procedures computing eq.
>
> The other problem with Dmitry's earlier suggestion is that the sets he's
> talking about could be infinite in size (at least in principle).
Exactly, but it is a problem with your definition of value, not with mine.
To me, as I said before, value does not belong to the language. Thus it is
not the language's problem to establish if two values are same. If the
programmer cares, he may declare operation "=" and implement it according
to the semantics of the problem space. If I wanted a type which values were
cardinal numbers aleph-0, aleph-1 etc, no problem with that.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-16 19:16 ` Dmitry A. Kazakov
@ 2013-05-16 21:59 ` Georg Bauhaus
2013-05-17 19:57 ` Dmitry A. Kazakov
0 siblings, 1 reply; 202+ messages in thread
From: Georg Bauhaus @ 2013-05-16 21:59 UTC (permalink / raw)
On 16.05.13 21:16, Dmitry A. Kazakov wrote:
> If the
> programmer cares, he may declare operation "=" and implement it according
> to the semantics of the problem space.
The little "implement" in the preceding sentence might require
comparing functions, which again is part of a problem.
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-16 21:59 ` Georg Bauhaus
@ 2013-05-17 19:57 ` Dmitry A. Kazakov
0 siblings, 0 replies; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-17 19:57 UTC (permalink / raw)
On Thu, 16 May 2013 23:59:14 +0200, Georg Bauhaus wrote:
> On 16.05.13 21:16, Dmitry A. Kazakov wrote:
>> If the
>> programmer cares, he may declare operation "=" and implement it according
>> to the semantics of the problem space.
>
> The little "implement" in the preceding sentence might require
> comparing functions, which again is part of a problem.
No more than implementing a flight control system, a database engine, an
image processing software etc.
All not the language's business, which was the point.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-16 18:09 ` Peter C. Chapin
2013-05-16 19:16 ` Dmitry A. Kazakov
@ 2013-05-16 21:20 ` Niklas Holsti
2013-05-16 23:20 ` Peter C. Chapin
1 sibling, 1 reply; 202+ messages in thread
From: Niklas Holsti @ 2013-05-16 21:20 UTC (permalink / raw)
On 13-05-16 21:09 , Peter C. Chapin wrote:
> On Thu, 16 May 2013, G.B. wrote:
>
>> On 16.05.13 15:54, Dmitry A. Kazakov wrote:
>
>>>> I realize that equivalence of functions is a difficult concept in
>>>> general
>>> There is nothing difficult in that. A function is a set of pairs. Two
>>> sets
>>> are equal when contain same elements.
>>
>> I think the difficulty is that eq is not computable. For example,
>> if f1 and f2 are any Ada compilers, produce an algorithm that computes
>>
>> eq(f1, f2)
>>
>> Then, proceed to finding eq of procedures computing eq.
>
> The other problem with Dmitry's earlier suggestion is that the sets he's
> talking about could be infinite in size (at least in principle).
> Comparing infinite sets can't be done in finite time, of course,
But comparing finite descriptions (generator programs) of the sets could
perhaps be done in finite time.
> so it
> doesn't really solve the problem in the general case. This is part of
> being not computable. I believe computing the equivalence of functions
> is undecidable, but I don't have a proof off hand (maybe one could be
> looked up).
A proof seems simple enough, assuming that the set of inputs is infinite
and enumerable: if you want to decide whether f1 and f2 are equivalent,
make a program P that iteratively generates (enumerates) all possible
inputs x; computes f1(x) and f2(x); and stops if f1(x) /= f2(x). This
program P halts if and only if f1 /= f2. Since halting is undecidable,
so therefore is function equality.
--
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
. @ .
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-16 21:20 ` Niklas Holsti
@ 2013-05-16 23:20 ` Peter C. Chapin
2013-05-17 5:25 ` Niklas Holsti
2013-05-17 7:53 ` Georg Bauhaus
0 siblings, 2 replies; 202+ messages in thread
From: Peter C. Chapin @ 2013-05-16 23:20 UTC (permalink / raw)
On Fri, 17 May 2013, Niklas Holsti wrote:
> A proof seems simple enough, assuming that the set of inputs is infinite
> and enumerable: if you want to decide whether f1 and f2 are equivalent,
> make a program P that iteratively generates (enumerates) all possible
> inputs x; computes f1(x) and f2(x); and stops if f1(x) /= f2(x). This
> program P halts if and only if f1 /= f2. Since halting is undecidable,
> so therefore is function equality.
You've shown that the method of enumerating all possible argument values
and testing f1(x) = f2(x) doesn't work. But perhaps there is some clever
way to statically analyze the code of f1 and f2 to decide their
equivalence without having to actually evaluate the functions for all
possible inputs.
I did a quick Google search on this out of curiosity and it turns out
there is a body of work in this area related to optimization. That makes
sense. Optimizers would like to make transformations on a given function
that generate provably equivalent functions (that are faster or smaller,
etc). It's easy to see why people into optimization would care about this.
I could imagine some sort of conversation that takes a function to a kind
of canonical form... maybe repeated applications of certain primitive
transformations on the code... and then showing equivalence would be a
matter of comparing the text of the canonical forms of the two functions.
I doubt it can be done (in general), but it's not immediately obvious to
me that it can't.
On the other hand, to prove undecidability one could use a reduction
approach. Assume I had a Turing machine program that could take as input
two functions (expressed also as Turing machine programs) <f1> and <f2>,
and accept that input if the two functions are equivalent, rejecting it
otherwise. Now show how one could transform an arbitrary instance of some
known undecidable problem, using a Turing machine and in finite time, to
an instance of the equivalence checking problem. If such a transformation
could be found, the equivalence checking problem would also be undecidable
since a solver for it would imply a solver for the original undecidable
problem.
Niklas, your approach actually does the reduction in the wrong direction.
You showed how one can transform an instance of the equivalence checking
problem into an instance of the halting problem. However, that doesn't
allow you to conclude equivalence checking is undecidable. Maybe that's
just the wrong way to do it.
Peter
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-16 23:20 ` Peter C. Chapin
@ 2013-05-17 5:25 ` Niklas Holsti
2013-05-17 7:53 ` Georg Bauhaus
1 sibling, 0 replies; 202+ messages in thread
From: Niklas Holsti @ 2013-05-17 5:25 UTC (permalink / raw)
On 13-05-17 02:20 , Peter C. Chapin wrote:
> On Fri, 17 May 2013, Niklas Holsti wrote:
>
>> A proof seems simple enough, assuming that the set of inputs is
>> infinite and enumerable: if you want to decide whether f1 and f2 are
>> equivalent, make a program P that iteratively generates (enumerates)
>> all possible inputs x; computes f1(x) and f2(x); and stops if f1(x) /=
>> f2(x). This program P halts if and only if f1 /= f2. Since halting is
>> undecidable, so therefore is function equality.
>
> You've shown that the method of enumerating all possible argument values
> and testing f1(x) = f2(x) doesn't work.
Yes, my argument is wrong (the reduction should go the other way). I
tried to cancel my post, but too late.... sorry.
I should not try to write proofs of undecidability at one hour past
midnight.
--
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
. @ .
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-16 23:20 ` Peter C. Chapin
2013-05-17 5:25 ` Niklas Holsti
@ 2013-05-17 7:53 ` Georg Bauhaus
1 sibling, 0 replies; 202+ messages in thread
From: Georg Bauhaus @ 2013-05-17 7:53 UTC (permalink / raw)
On 17.05.13 01:20, Peter C. Chapin wrote:
> On Fri, 17 May 2013, Niklas Holsti wrote:
>
>> A proof ...
Here is one (hint?), from 0122063821 Ch 16, 4. I am abbreviating,
as I guess you academics wouldn't want to see the level of detail
and context that the authors have added for laymen like myself:
Let
eq : N[⊥] × N[⊥] → N[⊥]
eq(x, y) = { 1 if x = y
{ 0 if x /= y
(eq is not monotonic, compare eq(⊥, ⊥) to eq(⊥, 0).) Let Φ[⊥] be
the strict extension of the universal function Φ(x, y) (which
takes y to be a program number), let ZERO[⊥] be the strict extension
of ZERO(x) = 0.
HALT(x, y) = eq(0, ZERO[⊥]( Φ[⊥](x, y) ))
"If ZERO[⊥] and Φ[⊥] are partially computable, then eq certainly
is not".
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-16 11:31 ` Peter C. Chapin
2013-05-16 11:56 ` Yannick Duchêne (Hibou57)
2013-05-16 12:20 ` Dmitry A. Kazakov
@ 2013-05-16 13:09 ` Eryndlia Mavourneen
2 siblings, 0 replies; 202+ messages in thread
From: Eryndlia Mavourneen @ 2013-05-16 13:09 UTC (permalink / raw)
On Thursday, May 16, 2013 6:31:58 AM UTC-5, Peter C. Chapin wrote:
> ...
> In the more general case there would be "task operators" that
> would allow you to compose tasks to make new tasks (higher order tasks?)
> and you would be able to store different tasks into the same variable of
> task type provided all the tasks had the same type (but possibly different
> bodies). Of course this language isn't Ada.
>
> That said, the Ada 2005 features of synchronized and protected interfaces
> are moving into this terrian. A full theoretical accounting of Ada task
> types would be a very interesting exercise (has it been done?).
> ...
> Peter
Yes, indeed! In a project of my own that I work on in my nearly negligible spare time, I use a number of task interfaces representing possible features of a service and compose the specific service I desire using a mix of these interfaces. Some interfaces are required by virtually every service, however most are not. This is one method to trim the size of the individual services, instead of trying to shoe-horn many unused features into a single task.
Eryndlia Mavourneen
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 6:37 ` Dmitry A. Kazakov
2013-05-11 7:06 ` Georg Bauhaus
@ 2013-05-11 7:58 ` Yannick Duchêne (Hibou57)
2013-05-11 9:08 ` Dmitry A. Kazakov
2013-05-11 18:14 ` Niklas Holsti
2013-05-11 8:03 ` Yannick Duchêne (Hibou57)
2 siblings, 2 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-11 7:58 UTC (permalink / raw)
Le Sat, 11 May 2013 08:37:15 +0200, Dmitry A. Kazakov
<mailbox@dmitry-kazakov.de> a écrit:
> That applies to stateful types only. Not every type is stateful. Bringing
> state into objects is considered bad practice. So bad, that it motivated
> some people to invent whole programming paradigms to avoid stateful
> object,
> e.g. functional programming. The sole idea of FP is to sweep states under
> the carpet.
FP is about expression without side effects (pure expression), not about
refusing to express states. There is no issue to have expressions
representing states and functions returning a state from a state, or even
expressions representing state transition. That's not an FP matter, but a
domain matter.
I've never seen so far, a paper about avoiding states in FP (what would be
state in FP anywhere, it not defined by the domain?). Else, out of
curiosity, I would welcome a pointer.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 7:58 ` Yannick Duchêne (Hibou57)
@ 2013-05-11 9:08 ` Dmitry A. Kazakov
2013-05-11 18:14 ` Niklas Holsti
1 sibling, 0 replies; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-11 9:08 UTC (permalink / raw)
On Sat, 11 May 2013 09:58:38 +0200, Yannick Duch�ne (Hibou57) wrote:
> Le Sat, 11 May 2013 08:37:15 +0200, Dmitry A. Kazakov
> <mailbox@dmitry-kazakov.de> a �crit:
>> That applies to stateful types only. Not every type is stateful. Bringing
>> state into objects is considered bad practice. So bad, that it motivated
>> some people to invent whole programming paradigms to avoid stateful object,
>> e.g. functional programming. The sole idea of FP is to sweep states under
>> the carpet.
>
> FP is about expression without side effects (pure expression), not about
> refusing to express states.
Side effect here = object[s] state.
[You certainly cannot attribute it to the control flow state as you return
to the definite point after expression is computed.]
> There is no issue to have expressions
> representing states and functions returning a state from a state,
You return values not states. State of the object is the value it presently
represents. State of flow is the source code location.
> I've never seen so far, a paper about avoiding states in FP (what would be
> state in FP anywhere, it not defined by the domain?). Else, out of
> curiosity, I would welcome a pointer.
FP-guys usually refuse to mention objects for evident reasons.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 7:58 ` Yannick Duchêne (Hibou57)
2013-05-11 9:08 ` Dmitry A. Kazakov
@ 2013-05-11 18:14 ` Niklas Holsti
1 sibling, 0 replies; 202+ messages in thread
From: Niklas Holsti @ 2013-05-11 18:14 UTC (permalink / raw)
On 13-05-11 10:58 , Yannick Duchêne (Hibou57) wrote:
> Le Sat, 11 May 2013 08:37:15 +0200, Dmitry A. Kazakov
> <mailbox@dmitry-kazakov.de> a écrit:
>> That applies to stateful types only. Not every type is stateful. Bringing
>> state into objects is considered bad practice. So bad, that it motivated
>> some people to invent whole programming paradigms to avoid stateful
>> object,
>> e.g. functional programming. The sole idea of FP is to sweep states under
>> the carpet.
>
> FP is about expression without side effects (pure expression), not about
> refusing to express states. There is no issue to have expressions
> representing states and functions returning a state from a state, or
> even expressions representing state transition. That's not an FP matter,
> but a domain matter.
>
> I've never seen so far, a paper about avoiding states in FP (what would
> be state in FP anywhere, it not defined by the domain?). Else, out of
> curiosity, I would welcome a pointer.
Monads? http://en.wikipedia.org/wiki/Monad_%28functional_programming%29
--
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
. @ .
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 6:37 ` Dmitry A. Kazakov
2013-05-11 7:06 ` Georg Bauhaus
2013-05-11 7:58 ` Yannick Duchêne (Hibou57)
@ 2013-05-11 8:03 ` Yannick Duchêne (Hibou57)
2013-05-11 9:16 ` Dmitry A. Kazakov
2 siblings, 1 reply; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-11 8:03 UTC (permalink / raw)
Le Sat, 11 May 2013 08:37:15 +0200, Dmitry A. Kazakov
<mailbox@dmitry-kazakov.de> a écrit:
> First of all, there are preconditions of operations and the precondition
> put on individual calls. I don't know which one you mean here. But the
> preconditions of operations must be statically true.
That's the point I don't understand or can't visualize: “preconditions of
operations must be statically true”. Out of any context? Or else, do you
suggest to move all the constraints on the types used by the operations?
(if so, that's just delegating or moving the condition elsewhere, isn't
it?).
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 8:03 ` Yannick Duchêne (Hibou57)
@ 2013-05-11 9:16 ` Dmitry A. Kazakov
2013-05-11 11:49 ` Georg Bauhaus
2013-05-11 22:51 ` Robert A Duff
0 siblings, 2 replies; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-11 9:16 UTC (permalink / raw)
On Sat, 11 May 2013 10:03:13 +0200, Yannick Duchêne (Hibou57) wrote:
> Le Sat, 11 May 2013 08:37:15 +0200, Dmitry A. Kazakov
> <mailbox@dmitry-kazakov.de> a écrit:
>> First of all, there are preconditions of operations and the precondition
>> put on individual calls. I don't know which one you mean here. But the
>> preconditions of operations must be statically true.
>
> That's the point I don't understand or can't visualize: “preconditions of
> operations must be statically true”. Out of any context?
Yep. The reason for that is that the designed of an operation cannot
control or even foresee the contexts where the operation will be used. It
is neither his responsibility nor his concern.
> Or else, do you
> suggest to move all the constraints on the types used by the operations?
I suggest that properly designed types should have no constraints of this
kind.
> (if so, that's just delegating or moving the condition elsewhere, isn't
> it?).
The condition is moved to the post-condition. E.g.
# require X >= 0.0
function sqrt (X : Float) return Float;
# ensure sqrt (X)**2 = X
is replaced with
# require true
function sqrt (X : Float) return Float;
# ensure sqrt (X)**2 = X or else Constraint_Error raised
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 9:16 ` Dmitry A. Kazakov
@ 2013-05-11 11:49 ` Georg Bauhaus
2013-05-11 12:25 ` Dmitry A. Kazakov
2013-05-11 22:51 ` Robert A Duff
1 sibling, 1 reply; 202+ messages in thread
From: Georg Bauhaus @ 2013-05-11 11:49 UTC (permalink / raw)
"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:
> The condition is moved to the post-condition. E.g.
>
> # require X >= 0.0
> function sqrt (X : Float) return Float;
> # ensure sqrt (X)**2 = X
>
> is replaced with
>
> # require true
> function sqrt (X : Float) return Float;
> # ensure sqrt (X)**2 = X or else Constraint_Error raised
So sqrt tests X for being non-negative and raises C_E otherwise?
Can the test be turned off?
# require true
procedure increase_pressure (P : in out Pot; X : Float);
# ensure pressure (P) = X * pressure (P'old) or else Kaboom raised
So where goes the precondition of the second kind mentioned
earlier, for calls, the one that is needed for correctness of the program?
I take it that the former kind of precondition prevents Kaboom in the
system?
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 11:49 ` Georg Bauhaus
@ 2013-05-11 12:25 ` Dmitry A. Kazakov
0 siblings, 0 replies; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-11 12:25 UTC (permalink / raw)
On 11 May 2013 11:49:12 GMT, Georg Bauhaus wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote:
>
>> The condition is moved to the post-condition. E.g.
>>
>> # require X >= 0.0
>> function sqrt (X : Float) return Float;
>> # ensure sqrt (X)**2 = X
>>
>> is replaced with
>>
>> # require true
>> function sqrt (X : Float) return Float;
>> # ensure sqrt (X)**2 = X or else Constraint_Error raised
>
> So sqrt tests X for being non-negative and raises C_E otherwise?
> Can the test be turned off?
It is not test, it is a behavior. However if sqrt were inlined, at least
partially, one branch of "if" could be removed if its condition proved
static.
> # require true
> procedure increase_pressure (P : in out Pot; X : Float);
> # ensure pressure (P) = X * pressure (P'old) or else Kaboom raised
>
> So where goes the precondition of the second kind mentioned
> earlier, for calls, the one that is needed for correctness of the program?
Is it a physical system you are talking about? In that case it does not
work this way. You have a hardware in the [control] loop (HIL). E.g. a
valve, a boiler, whatever. You set the valve using an actuator, you control
its position using position sensors, you control pressure using pressure
sensors, you control things using indirect measures, e.g. of the
temperature etc. There is a model of the system according to which you act
and react. It is very different from digital deterministic systems where
cause and effect are tied to the point of being equivalent.
> I take it that the former kind of precondition prevents Kaboom in the
> system?
By not raising it. So long the model is adequate [as estimated though the
sensors] you don't raise anything. When the model is no more adequate you
drive the system into a definite state as specified by the requirements,
e.g. by doing an emergency shutdown. This procedure may be implemented
using exceptions. In some cases definite state is achieved by self
destruction (see Ariane).
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 9:16 ` Dmitry A. Kazakov
2013-05-11 11:49 ` Georg Bauhaus
@ 2013-05-11 22:51 ` Robert A Duff
2013-05-12 6:02 ` Dmitry A. Kazakov
1 sibling, 1 reply; 202+ messages in thread
From: Robert A Duff @ 2013-05-11 22:51 UTC (permalink / raw)
"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> The condition is moved to the post-condition. E.g.
>
> # require X >= 0.0
> function sqrt (X : Float) return Float;
> # ensure sqrt (X)**2 = X
>
> is replaced with
>
> # require true
> function sqrt (X : Float) return Float;
> # ensure sqrt (X)**2 = X or else Constraint_Error raised
It seems to me that this replacement loses information (the info that
X is "supposed to be nonnegative").
For example, a body of sqrt that says "return X / 0.0;" obeys the second
contract but not the first above. But that's obviously wrong to anyone
who thinks that "sqrt" means "approximate square root of X".
(Never mind the accuracy issues -- sqrt(X) might not be representable as
a Float. ;-) )
- Bob
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 22:51 ` Robert A Duff
@ 2013-05-12 6:02 ` Dmitry A. Kazakov
2013-05-12 6:25 ` Yannick Duchêne (Hibou57)
0 siblings, 1 reply; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-12 6:02 UTC (permalink / raw)
On Sat, 11 May 2013 18:51:27 -0400, Robert A Duff wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>
>> The condition is moved to the post-condition. E.g.
>>
>> # require X >= 0.0
>> function sqrt (X : Float) return Float;
>> # ensure sqrt (X)**2 = X
>>
>> is replaced with
>>
>> # require true
>> function sqrt (X : Float) return Float;
>> # ensure sqrt (X)**2 = X or else Constraint_Error raised
>
> It seems to me that this replacement loses information (the info that
> X is "supposed to be nonnegative").
# ensure
(X >= 0.0 and then sqrt (X)**2 = X)
or else
(X < 0.0 and then Constraint_Error raised)
> For example, a body of sqrt that says "return X / 0.0;" obeys the second
> contract but not the first above. But that's obviously wrong to anyone
> who thinks that "sqrt" means "approximate square root of X".
As "approximate square root" any implementation is OK. A more realistic
contract that defines accuracy of the result could be like:
sqrt (X)**2 in Float'Max (0.0, X'Pred)..Float'Min (Float'Last, X'Succ)
[It was just an illustration of the idea how preconditions of operations
are relaxed.]
> (Never mind the accuracy issues -- sqrt(X) might not be representable as
> a Float. ;-) )
No, because sqrt(X) < X, if X > 0.
But considering mathematical sqrt, yes, it is not even complex-valued. sqrt
is a multi-valued complex function. If we are lucky one value of sqrt(X)
might have zero imaginary part.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-12 6:02 ` Dmitry A. Kazakov
@ 2013-05-12 6:25 ` Yannick Duchêne (Hibou57)
2013-05-12 7:14 ` Dmitry A. Kazakov
0 siblings, 1 reply; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-12 6:25 UTC (permalink / raw)
Le Sun, 12 May 2013 08:02:16 +0200, Dmitry A. Kazakov
<mailbox@dmitry-kazakov.de> a écrit:
>>> The condition is moved to the post-condition. E.g.
>>>
>>> # require X >= 0.0
>>> function sqrt (X : Float) return Float;
>>> # ensure sqrt (X)**2 = X
>>>
>>> is replaced with
>>>
>>> # require true
>>> function sqrt (X : Float) return Float;
>>> # ensure sqrt (X)**2 = X or else Constraint_Error raised
>>
>> It seems to me that this replacement loses information (the info that
>> X is "supposed to be nonnegative").
>
> # ensure
> (X >= 0.0 and then sqrt (X)**2 = X)
> or else
> (X < 0.0 and then Constraint_Error raised)
But what's the benefit of moving the precondition to the postcondition? Or
more simply, why dropping the idea of precondition for sub‑program
declarations?
Do you have to re‑invent or re‑derive the precondition at each call place,
from the postcondition? Isn't it kind of bloat?
It makes more me feel like losing something than the opposite. And how do
you clearly connect valid invocations into sequence? You can't connect any
more, the post condition of A to precondition of B (when B comes next to
A), or else, less clearly. There may be an issue with separation of
concern here (the God postcondition?). I won't enjoy a variant of Ada
doing so.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-12 6:25 ` Yannick Duchêne (Hibou57)
@ 2013-05-12 7:14 ` Dmitry A. Kazakov
2013-05-12 7:37 ` Simon Wright
2013-05-12 8:21 ` Yannick Duchêne (Hibou57)
0 siblings, 2 replies; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-12 7:14 UTC (permalink / raw)
On Sun, 12 May 2013 08:25:33 +0200, Yannick Duchêne (Hibou57) wrote:
> Le Sun, 12 May 2013 08:02:16 +0200, Dmitry A. Kazakov
> <mailbox@dmitry-kazakov.de> a écrit:
>>>> The condition is moved to the post-condition. E.g.
>>>>
>>>> # require X >= 0.0
>>>> function sqrt (X : Float) return Float;
>>>> # ensure sqrt (X)**2 = X
>>>>
>>>> is replaced with
>>>>
>>>> # require true
>>>> function sqrt (X : Float) return Float;
>>>> # ensure sqrt (X)**2 = X or else Constraint_Error raised
>>>
>>> It seems to me that this replacement loses information (the info that
>>> X is "supposed to be nonnegative").
>>
>> # ensure
>> (X >= 0.0 and then sqrt (X)**2 = X)
>> or else
>> (X < 0.0 and then Constraint_Error raised)
>
> But what's the benefit of moving the precondition to the postcondition? Or
> more simply, why dropping the idea of precondition for sub‑program
> declarations?
In short, because it is inconsistent with the notion of type. Other issues
are merely consequences.
> Do you have to re‑invent or re‑derive the precondition at each call place,
> from the postcondition?
Conditions at call place are of second kind. They could be any or none.
> It makes more me feel like losing something than the opposite. And how do
> you clearly connect valid invocations into sequence?
See above, it is 1st and 2nd kind conditions. You are conflating the
semantics of a type with the semantics of *a* program that uses this type
somewhere, somehow.
To put it simply: if a type is designed in a way that limits it use, it is
a poor design.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-12 7:14 ` Dmitry A. Kazakov
@ 2013-05-12 7:37 ` Simon Wright
2013-05-12 7:59 ` Dmitry A. Kazakov
2013-05-12 8:21 ` Yannick Duchêne (Hibou57)
1 sibling, 1 reply; 202+ messages in thread
From: Simon Wright @ 2013-05-12 7:37 UTC (permalink / raw)
"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> To put it simply: if a type is designed in a way that limits it use,
> it is a poor design.
I think that depends on who is paying for all the extra work you would
be putting in.
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-12 7:37 ` Simon Wright
@ 2013-05-12 7:59 ` Dmitry A. Kazakov
0 siblings, 0 replies; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-12 7:59 UTC (permalink / raw)
On Sun, 12 May 2013 08:37:11 +0100, Simon Wright wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>
>> To put it simply: if a type is designed in a way that limits it use,
>> it is a poor design.
>
> I think that depends on who is paying for all the extra work you would
> be putting in.
Not much. If you can formalize the constraint to the level which would
allow its specification as a precondition, then you also can as easily
remove it from there.
On the other hand, considering all sorts of write once run once designs, it
would be quite strange to expect that people doing that would pay any
attention to writing preconditions.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-12 7:14 ` Dmitry A. Kazakov
2013-05-12 7:37 ` Simon Wright
@ 2013-05-12 8:21 ` Yannick Duchêne (Hibou57)
2013-05-12 9:25 ` Dmitry A. Kazakov
1 sibling, 1 reply; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-12 8:21 UTC (permalink / raw)
Le Sun, 12 May 2013 09:14:41 +0200, Dmitry A. Kazakov
<mailbox@dmitry-kazakov.de> a écrit:
> To put it simply: if a type is designed in a way that limits it use, it
> is
> a poor design.
The sense or meaning, both in natural and formal languages, comes from
restricting possible interpretations.
> You are conflating the
> semantics of a type with the semantics of *a* program that uses this type
> somewhere, somehow.
Precisely, I see types as constituents of a domain, so also as
constituents of applications of the domain. I'm guessing I'm not the only
one.
We may diverge here, in short I would say: I don't want bricks giving the
illusions I may always be able to use it to build something which may or
may not fails, I want bricks which will tell the sooner I will not be able
to use it in some invalid ways if I want something which will not fail (or
at least reduce potentials for failures, as program proof is more than
that).
What I don't understand is: how something which give the illusion it has
no prerequisites, can help in constructing safer and more trustable
architectures? Reusing is nice, however only where it, and in a way which,
make sense for the domain (I don't believe an exception is meaningful,
that's not a value, that's a runtime error). Seems the invariably `True`
precondition wants to give the illusion of universal reuse without
conditions. With all precondition moved to the postcondition, the program
has more potential for erroneous interpretation, because that may turns
into a lot more decision paths in the program after each invocation.
I will not argue that much on this issue, as that may involves personal
feeling.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-12 8:21 ` Yannick Duchêne (Hibou57)
@ 2013-05-12 9:25 ` Dmitry A. Kazakov
2013-05-12 9:32 ` Yannick Duchêne (Hibou57)
0 siblings, 1 reply; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-12 9:25 UTC (permalink / raw)
On Sun, 12 May 2013 10:21:49 +0200, Yannick Duchêne (Hibou57) wrote:
> We may diverge here, in short I would say: I don't want bricks giving the
> illusions I may always be able to use it to build something which may or
> may not fails, I want bricks which will tell the sooner I will not be able
> to use it in some invalid ways if I want something which will not fail (or
> at least reduce potentials for failures, as program proof is more than
> that).
It is impossible to achieve. It also contradicts the basic principle of
design: divide and conquer. You want bricks to learn architecture? Even if
that were possible such bricks would be unaffordable. And how would you
validate, test, certify such bricks?
> What I don't understand is: how something which give the illusion it has
> no prerequisites, can help in constructing safer and more trustable
> architectures?
Simplicity, abstraction, Occam's razor, the principle of minimum energy,
basic customs of engineering etc.
> Seems the invariably `True`
> precondition wants to give the illusion of universal reuse without
> conditions.
No, "true" means what that the contract was not a lie. If you say that the
argument of sqrt is Float and another person say that it is not negative,
then somebody is lying here.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-12 9:25 ` Dmitry A. Kazakov
@ 2013-05-12 9:32 ` Yannick Duchêne (Hibou57)
2013-05-12 10:07 ` Dmitry A. Kazakov
0 siblings, 1 reply; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-12 9:32 UTC (permalink / raw)
Le Sun, 12 May 2013 11:25:51 +0200, Dmitry A. Kazakov
<mailbox@dmitry-kazakov.de> a écrit:
>> Seems the invariably `True`
>> precondition wants to give the illusion of universal reuse without
>> conditions.
>
> No, "true" means what that the contract was not a lie. If you say that
> the
> argument of sqrt is Float and another person say that it is not negative,
> then somebody is lying here.
This is the same person who says both as this is the one who wrote the
signature and the precondition. And this is not a contradiction to have
conjunction of conditions, that's common.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-12 9:32 ` Yannick Duchêne (Hibou57)
@ 2013-05-12 10:07 ` Dmitry A. Kazakov
0 siblings, 0 replies; 202+ messages in thread
From: Dmitry A. Kazakov @ 2013-05-12 10:07 UTC (permalink / raw)
On Sun, 12 May 2013 11:32:13 +0200, Yannick Duchêne (Hibou57) wrote:
> Le Sun, 12 May 2013 11:25:51 +0200, Dmitry A. Kazakov
> <mailbox@dmitry-kazakov.de> a écrit:
>
>>> Seems the invariably `True`
>>> precondition wants to give the illusion of universal reuse without
>>> conditions.
>>
>> No, "true" means what that the contract was not a lie. If you say that the
>> argument of sqrt is Float and another person say that it is not negative,
>> then somebody is lying here.
>
> This is the same person who says both as this is the one who wrote the
> signature and the precondition. And this is not a contradiction to have
> conjunction of conditions, that's common.
Except that it is not a conjunction. If it were a conjunction then either
specified as proper type or else, if there were no types, as solely a
dynamic precondition. That is the choice between being untyped or strong
types. Your case is neither. Furthermore it cannot be made the second in
realistic cases because such constraints cannot be statically enforced. So
if you want it a conjunction it must be the first:
# pre X in Float and then X >= 0.0
function sqrt (X : Any) return Float;
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 0:42 ` Randy Brukardt
2013-05-11 6:37 ` Dmitry A. Kazakov
@ 2013-05-11 7:32 ` Yannick Duchêne (Hibou57)
2013-05-11 7:46 ` Yannick Duchêne (Hibou57)
2 siblings, 0 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-11 7:32 UTC (permalink / raw)
Le Sat, 11 May 2013 02:42:37 +0200, Randy Brukardt <randy@rrsoftware.com>
a écrit:
>> 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.
As often, depends on the use case and domain (with proofs and analysis,
substitutability is important).
Was just thinking about something to please both: don't see
substitutability as a requirement, but as something optionally provided;
there could be a way to assert substitutability when something can provide
it, while not requiring it all the time. That would be a kind of
noticeable property which could be explicitly created and asserted.
There are people who need it, there are others who really don't care.
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Re: Seeking for papers about tagged types vs access to subprograms
2013-05-11 0:42 ` Randy Brukardt
2013-05-11 6:37 ` Dmitry A. Kazakov
2013-05-11 7:32 ` Yannick Duchêne (Hibou57)
@ 2013-05-11 7:46 ` Yannick Duchêne (Hibou57)
2 siblings, 0 replies; 202+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2013-05-11 7:46 UTC (permalink / raw)
Le Sat, 11 May 2013 02:42:37 +0200, Randy Brukardt <randy@rrsoftware.com>
a écrit:
> 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.
Well, “they use” or “they provides” or “they comes with”, ends to be all
the same: that's a system of interdependent things. A type may depends on
a function to create its instances, at least in the public view, as much
as sub‑programs depends on types, and there are optional and required
dependencies (if optional, better in child or other packages).
To be checked: do all formalism use functions and types at their core
basis or are there some formalisms which only uses functions and defines
types in terms of functions (I will check it a future day, I believe the
latter is the is true, while not sure).
--
“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
^ permalink raw reply [flat|nested] 202+ messages in thread
* Weaker typing as a part of the way to stronger typing? (Was: Seeking for papers about tagged types vs access to subprograms)
2013-05-09 22:19 ` Randy Brukardt
` (4 preceding siblings ...)
2013-05-10 7:48 ` Dmitry A. Kazakov
@ 2013-05-14 12:46 ` Jacob Sparre Andersen
2013-05-14 19:08 ` Randy Brukardt
5 siblings, 1 reply; 202+ messages in thread
From: Jacob Sparre Andersen @ 2013-05-14 12:46 UTC (permalink / raw)
Randy Brukardt wrote:
> Dmitry A. Kazakov wrote:
[ Nothing whatsoever about access to subprograms. - Please update the
subject line to match what you are writing about. It makes it much
easier for everybody to follow you. ]
>> 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.
Considering that SPARK on one level is rather un-typed (all numbers seem
to be equivalent on the constraint error checking level of SPARK), you
may be onto something. But how would avoid making a monster like Java,
where programmers can use weak types everywhere (except as the main
subprogram).
> 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.
Might be right. But how would you separate operations on the
representation level from operations on the typed ("profile") level?
Greetings,
Jacob
--
"... there may be many others,
but they haven't been discovered" -- Tom Lehrer
^ permalink raw reply [flat|nested] 202+ messages in thread* Re: Weaker typing as a part of the way to stronger typing? (Was: Seeking for papers about tagged types vs access to subprograms)
2013-05-14 12:46 ` Weaker typing as a part of the way to stronger typing? (Was: Seeking for papers about tagged types vs access to subprograms) Jacob Sparre Andersen
@ 2013-05-14 19:08 ` Randy Brukardt
0 siblings, 0 replies; 202+ messages in thread
From: Randy Brukardt @ 2013-05-14 19:08 UTC (permalink / raw)
"Jacob Sparre Andersen" <jacob.sparre@koparo.com> wrote in message
news:871u99ohk7.fsf_-_@adaheads.sparre-andersen.dk...
> Randy Brukardt wrote:
>> Dmitry A. Kazakov wrote:
>
> [ Nothing whatsoever about access to subprograms. - Please update the
> subject line to match what you are writing about. It makes it much
> easier for everybody to follow you. ]
>
>>> 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.
>
> Considering that SPARK on one level is rather un-typed (all numbers seem
> to be equivalent on the constraint error checking level of SPARK), you
> may be onto something. But how would avoid making a monster like Java,
> where programmers can use weak types everywhere (except as the main
> subprogram).
>
>> 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.
>
> Might be right. But how would you separate operations on the
> representation level from operations on the typed ("profile") level?
I don't think there are any operations on the representation level (well,
maybe a small number, like the predefined numeric operations in Ada). I
would guess that such operations would have an empty profile (meaning
they're always applicable), while most operations would have profiles that
would restrict their applicability.
In any case, these are the questions for a new language design. If they are
already clearly answered, we wouldn't need a new language!
Randy.
^ permalink raw reply [flat|nested] 202+ messages in thread