Scott, > how significant > are the differences between sets & types? For example, Z is > very obviously based on set theory and is a powerful, expressive > language. Are there limitations imposed on it by its set-theoretic > underpinnings that would not exist in a type-theoretic counterpart? You may find "Type inference for set-theory" by Ray Turner, Theoretical Computer Science 266 (2001) 951-974 of interest. Martin Henson