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

[Van Snyder]

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.

> Mike gets into an infinite loop by assuming the types of A and B are not
> equivalent, so when he arrives at TYPE(T), POINTER :: NEXT he knows he's
> been there, but not that the T's are equivalent, so he dives into their
> graphs.
>