Home » forums » LtU Forum

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 | previous forum topic | next forum topic | other blogs | 5844 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Subtyping with dependent types has been studied in the literatur

You should have a look at David Aspinall and Adriana Compagnoni's 1006-2000 work: Subtyping Dependent Types (and his related work on singleton types and dependent types). He discusses subtyping in presence of dependent types, but does not study variance because his dependent system does not have type-level abstraction.

For discussion of variance in type-level abstraction, see the work on "polarized higher-order subtyping", in particular Martin Steffen's 1997 PhD thesis.

One should also cite the work on "coercive subtyping" by Zhaohui Luo, for example his 1999 journal article on dependent coercions.

I don't know about your use of Curry-Howard to define subtyping; I'm not sure it brings much. In systems with subtyping, you usually have a syntactic judgement that defines subtyping through inference rules. You suggest to replace this by a reasoning system in the logic to decide which propositions can be "derived" from another. If your reasoning system for "can be derived from" is also syntactic, it looks like you will have the exact same thing. If one see coercions as term-level witnesses of subtyping relations, one could say, I guess, that they are proof terms for your "can be derived from" relation.

By gasche at Sat, 2012-05-05 10:17 | login or register to post comments