Dependent C-style types with subtyping rule

Question

I'm looking for previous work regarding an extension of a C-style type system in which types may have constraints and have a defined subtyping rule. In particular, I'm interested in defining algebra-like rules for types on which an order relation exists.

I will use integers for the rest of the examples, but those could be swapped for any kind of object that defines a total order relation.

Right now, I have a system that allows me to define a type as being a pair $(T, \phi)$ where $T$ is a "basic" C-style type (not a pointer, for instance) and $\phi$ is a constraint expressed in a simple language that is basically an extension of propositional calculus. For example, $(\texttt{int}, (>30)\ \text{and}\ (<40))$ would represent the type of integers between 30 and 40. This is similar to what happens in Dependent types, but is significantly less expressive.

I also define a subtyping rule based on the Liskov substitution principle, that specifies that given two types $\mathcal{T}_1 := (T, \phi_1)$ and $\mathcal{T}_2 := (T, \phi_2)$, $\phi_1 \vdash \phi_2 \implies \mathcal{T}_1 <: \mathcal{T}_2$. For instance, $$ (\texttt{int}, (>30)\ \text{and}\ (<40)) <: (\texttt{int}, (>0)\ \text{and}\ (<100)) $$

For my needs, I am not interested in equivalence or isomorphism between types, only subtyping. I believe that by such "reductions", this flavour of dependent typing can be proved to be decidable.

I've been searching for previous works regarding something similar to what I have right now, but most of the works seem to focus on higher-order lambda calculus. This thread lists various articles regarding such works.

I'm struggling understand what to look for, as I do not know how such a system could be described, because "dependent types" and "subtyping" are obviously very broad fields and lead me to very general papers, while I'd like to find something that is more specific and less expressive.

EDIT: To clarify, the "C-style type" enhanced by a formula is generally a numeric data type, but could be struct if the struct were to define an order relation. I'm not specifically looking for anything regarding arrays, but it would be a "nice to have".

Answer 1

I think the best setup here is Liquid Types, but compared to the original Liquid Types paper, you would want a much weaker language of constraints. Also, if you don't need type inference, it's even easier.

You'd still have to solve linear programs, though. Consider this function:

{int | (< 30) /\ (>= 10)} foo({int | (> 20)} bar, {int | (<= 70)} baz) {...} 

and you do some arithmetic on bar and baz inside the function. Then, to type check the function, you'd have to make sure that this expression takes a value between 10 and 29, which means you'd still need to solve linear programming (treating all non-constant multiplication as atoms), which is NP-complete. However, it is known that linear programming can be polynomial if you fix the number of variables involved. What implications do this fact have on our system? I don't really know as I'm not an expert in this area.

But I suspect what you really want is some sort of symbolic execution or abstract interpretation. If your language is completely first-order and doesn't have pointers, both should be pretty easy, and would involve far less human work (i.e. type annotations).