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?
Recent comments
6 weeks 18 hours ago
6 weeks 22 hours ago
6 weeks 22 hours ago
28 weeks 2 days ago
32 weeks 4 days ago
34 weeks 1 day ago
34 weeks 1 day ago
36 weeks 6 days ago
41 weeks 3 days ago
41 weeks 3 days ago