archives

Subtyping and dependent types

Hi,
I'm thinking about combining subtyping with dependent types, and would like to hear from the community if there's something similar already done or published.
My idea is to allow stablishing subtyping derivations for any new type. For polymorhphic types, the programmer is allows to specify whether each parameter is co or contra variant in relation with subtyping. Then, I would also like to say a type A is subtype of another B if the meaning of A via the proposition-as-types isomorphism can be derived from the meaning of B. Does it sound reasonable?

By serras at 2012-05-05 09:57 | LtU Forum | 1 comment | other blogs | 5546 reads