1
$\begingroup$

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".

$\endgroup$
  • 1
    $\begingroup$ What do you man by C-style types? C has pointer types, which are generally a bit difficult to reconcile with interesting type-safety properties. $\endgroup$ – Martin Berger Feb 26 at 10:56
  • $\begingroup$ @MartinBerger I've added some edits in regards to your comment. Indeed, pointers are a bit out of scope for my idea $\endgroup$ – Francesco Bertolaccini Feb 26 at 11:02
  • 2
    $\begingroup$ Could refinement types be what you are looking for? $\endgroup$ – Martin Berger Feb 26 at 11:28
  • $\begingroup$ @MartinBerger refinement types look interesting, I'll read up on them and I'll come back once I know something more about them $\endgroup$ – Francesco Bertolaccini Feb 26 at 12:41
  • $\begingroup$ Take a look at Dependent ML, it seems similar to what you're dealing with. $\endgroup$ – jmite Feb 26 at 15:10
1
$\begingroup$

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).

$\endgroup$
  • $\begingroup$ Liquid types are a special case of refinement types, no? $\endgroup$ – Martin Berger Mar 1 at 13:15
  • $\begingroup$ Your suggestion about symbolic execution/abstract interpretation may be spot on. I think I will be going in a "hybrid" direction, by employing symbolic execution as a way to manipulate the types. $\endgroup$ – Francesco Bertolaccini Mar 1 at 13:56
  • $\begingroup$ @MartinBerger Yes, definitely. I singled them out here because IMO their presentation is clear and understandable. $\endgroup$ – xrq Mar 1 at 20:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.