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
4 days 20 hours ago
40 weeks 6 days ago
40 weeks 6 days ago
40 weeks 6 days ago
1 year 10 weeks ago
1 year 15 weeks ago
1 year 16 weeks ago
1 year 16 weeks ago
1 year 19 weeks ago
1 year 24 weeks ago