Re: Literature needed on recursive (union) types

nico@dutiag.twi.tudelft.nl (Nico Plat) writes:


>Consider the two type definitons
>
> T1 = nat | nat X T1 { 'X' denotes a product type }
> T2 = real | real X T2
>
>IsSubType (nat, real) is defined to be true, and therefore it is easy
>to see that IsSubType (T1, T2) should be true as well. The obvious
>implementation does not work, however, because a recursive call to
>IsSubType (T1, T2) is made when examing the second component


Can't this be handled by contrafactuals? Start from the presumption
that T1 is a subtype of T2, and prove that this is consistent with
the actual type definitions. You can then break the recursion by
appealing to the assumption. As long as the individual types aren't
"viciously" recursive, there won't be a vicious circularity in the
comparison.
--

Return to the comp.compilers page.
Search the comp.compilers archives again.