(j3.2006) more on J32031 equivalence of circular types

[Robert Corbett]

Van Snyder wrote:
> On Wed, 2008-08-20 at 18:46 -0700, Van Snyder wrote:
> 
>>On Wed, 2008-08-20 at 15:19 -0700, Aleksandar Donev wrote:
>>
>>>On Wednesday 20 August 2008 15:15, Bill Long wrote:
>>>
>>>>I guess I don't see what part of the answer is not obvious here.  What
>>>>part of f03:4.5.1.3 is ambiguous in the case?
>>>
>>>TYPE(T), POINTER :: NEXT => NULL()
>>>
>>>Does this component in type T in module FOO have the same type as that in 
>>>module BAR? If you know the answer, you've already answered the question you 
>>>are trying to answer. You get into an infinite loop that you must terminate 
>>>somehow.
>>
>>The answer depends upon whether you start by assuming the types are
>>equivalent and try to prove they're not, or start by assuming the types
>>are different and try to prove they're equivalent.
>>
>>In the first case, you assume the types of A and B are equivalent.  Then
>>you start doing a simultaneous recursive traversal of both type systems'
>>graphs (type systems in the case of recursive types involving more than
>>one type).  When you arrive at types you've visited, you say "Aha! I've
>>been here, so they must be the same!"  If you arrive at anything
>>different in the traversals, you quit and say "No!"  If you finish
>>traversing the graphs by visiting every vertex without saying "No!", you
>>quit and say "Yes!"
> 
> 
> I don't think you have any choice but to say "Aha! I've been here so
> they must be the same" when the simultaneous traversals arrive at
> previously-visited types.  If they were different, the algorithm would
> already have quit with a "No" answer.

Oh dear.  This further response makes me wonder if I correctly
understood your previous response.  Your previous response is
correct in stating that different answers are produced depending
on whether you start by assuming that similar types are
equivalent or not.

Let's reduce the problem to the propositional calculus.  Consider
the two statements

     If P = P', then Q = Q'.

     If Q = Q', then P = P'.

Do these two statements provide enough information to decide whether
P = P'?  Others might disagree, but I think they do not.

Exactly that situation is demonstrated by the example I gave in my
comment on the subject.  If the types named T1 in the module and the
main program "agree,"  then the types named T2 in the module and the
main program also "agree."  If you assume that the types named T2 in
the module and the main program "agree," then the types named T1 in
the module and the main program also "agree."  If the types named T1
in the module and the main program do not "agree," then the types
named T2 in the module and the main program do not "agree."  If the
types named T2 in the module and the main program do not "agree,"
then the types named T1 in module and the main program do not "agree."
Either interpretation is consistent with the statements given in
Section 4.5.2.4 of CD 1539-1.  Therefore, the draft standard does not
provide enough information to decide if the types "agree."

Bob Corbett