Wed, 16 Sep 1992 11:52:47 GMT

Related articles |
---|

Literature needed on recursive (union) types nico@dutiag.twi.tudelft.nl (1992-09-15) |

Re: Literature needed on recursive (union) types firth@sei.cmu.edu (1992-09-16) |

Re: Literature needed on recursive (union) types drw@euclid.mit.edu (1992-09-16) |

Newsgroups: | comp.compilers |

From: | firth@sei.cmu.edu (Robert Firth) |

Organization: | Software Engineering Institute |

Date: | Wed, 16 Sep 1992 11:52:47 GMT |

References: | 92-09-079 |

Keywords: | types, design |

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.

--

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.