<p>I think the best setup here is <a href="http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf" rel="nofollow noreferrer">Liquid Types</a>, 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. </p>

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

<pre><code>{int | (&lt; 30) /\ (&gt;= 10)} foo({int | (&gt; 20)} bar, {int | (&lt;= 70)} baz) {...} 
</code></pre>

<p>and you do some arithmetic on <code>bar</code> and <code>baz</code> 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.</p>

<p>But I suspect what you <em>really</em> 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).</p>

CC BY-SA 4.0
2019-03-01T13:15:40.927Z
Liquid types are a special case of refinement types, no?
Martin Berger
CC BY-SA 4.0
2019-03-01T13:56:08.133Z
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.
Francesco Bertolaccini
CC BY-SA 4.0
2019-03-01T20:01:15.567Z
@MartinBerger Yes, definitely. I singled them out here because IMO their presentation is clear and understandable.
xrq
CC BY-SA 4.0
2019-03-01T00:21:57.437Z
2019-03-01T00:21:57.437Z
xrq
<p>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.</p>

<p>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.</p>

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

<p>I also define a subtyping rule based on the Liskov substitution principle, that specifies that given two types <span class="math-container">$\mathcal{T}_1 := (T, \phi_1)$</span> and <span class="math-container">$\mathcal{T}_2 := (T, \phi_2)$</span>, <span class="math-container">$\phi_1 \vdash \phi_2 \implies \mathcal{T}_1 &lt;: \mathcal{T}_2$</span>. For instance,
<span class="math-container">$$
(\texttt{int}, (&gt;30)\ \text{and}\ (&lt;40)) &lt;: (\texttt{int}, (&gt;0)\ \text{and}\ (&lt;100))
$$</span></p>

<p>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.</p>

<p>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. <a href="https://lists.seas.upenn.edu/pipermail/types-list/2017/001958.html" rel="nofollow noreferrer">This thread</a> lists various articles regarding such works.</p>

<p>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.</p>

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

CC BY-SA 4.0
2019-02-26T10:56:06.863Z
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.
Martin Berger
CC BY-SA 4.0
2019-02-26T11:02:26.110Z
@MartinBerger I've added some edits in regards to your comment. Indeed, pointers are a bit out of scope for my idea
Francesco Bertolaccini
CC BY-SA 4.0
2019-02-26T11:28:52.457Z
Could refinement types be what you are looking for?
Martin Berger
CC BY-SA 4.0
2019-02-26T12:41:00.590Z
@MartinBerger refinement types look interesting, I'll read up on them and I'll come back once I know something more about them
Francesco Bertolaccini
CC BY-SA 4.0
2019-02-26T15:10:55.153Z
Take a look at Dependent ML, it seems similar to what you're dealing with.
Joey Eremondi
CC BY-SA 4.0
2019-02-27T07:33:31.037Z
@jmite That's indeed probably as close as it's going to get, thank you! You should probably add it as an answer
Francesco Bertolaccini
CC BY-SA 4.0
2019-02-28T08:37:45.670Z
I think refinement types are exactly what you want.
xrq
CC BY-SA 4.0
2019-02-28T08:38:43.780Z
The state of art in this realm is definitely Liquid Haskell. Play with it and have fun hacking!
xrq
CC BY-SA 4.0
2019-02-28T09:00:43.277Z
@xuq01 the issue I've found with liquid types is that they are still basically dependent types and they require an SMT solver in most cases, I'm working on doing something that is decidable preferably in polynomial time
Francesco Bertolaccini
CC BY-SA 4.0
2019-02-28T16:46:14.750Z
@FrancescoBertolaccini I believe that as long as you have linear arithmetic constraints in types, you can't do it in polynomial time anymore (of course, unless P=NP). Integer programming is NP-complete, so if you allow arithmetic constraints in types, they might not be solvable in polynomial time.
xrq
CC BY-SA 4.0
2019-02-28T16:49:48.197Z
If you only allow the constraints of a very weak form, I suppose you can do it in polynomial time. But then you gain very little from the constraints on types.
xrq
CC BY-SA 4.0
2019-02-28T17:18:28.943Z
@xuq01 Linear arithmetic is not to be allowed, I plan on only providing "bound" constraints of the type I've shown in the examples. I believe the limitedness of the language would make it restrictive, yes, but also useful in some specific applications.
Francesco Bertolaccini
CC BY-SA 4.0
2019-03-01T00:01:10.373Z
@FrancescoBertolaccini Hm, I believe that you can still use the same setup. You still have Liquid Types, except that your language of constraints is highly constrained. This way you can replace the SMT solver with a built-in, less-capable solver. OTOH, if you don't have very complex constraints, maybe you're better off using symbolic execution or abstract interpretation, rather than extending the type system?
xrq
<lo.logic><type-systems><dependent-type>
Dependent C-style types with subtyping rule
Francesco Bertolaccini
# Dependent C-style types with subtyping rule

(Asked by: username_0 on 2019-02-26)

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](https://lists.seas.upenn.edu/pipermail/types-list/2017/001958.html) 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".

**Tags:** lo.logic, type-systems, dependent-type

> **Comments:**
> **username_1**: 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.  
> **username_0**: @MartinBerger I've added some edits in regards to your comment. Indeed, pointers are a bit out of scope for my idea  
> **username_1**: Could refinement types be what you are looking for?  
> **username_0**: @MartinBerger refinement types look interesting, I'll read up on them and I'll come back once I know something more about them  
> **username_2**: Take a look at Dependent ML, it seems similar to what you're dealing with.  
> **username_0**: @jmite That's indeed probably as close as it's going to get, thank you! You should probably add it as an answer  
> **username_3**: I think refinement types are exactly what you want.  
> **username_3**: The state of art in this realm is definitely Liquid Haskell. Play with it and have fun hacking!  
> **username_0**: @xuq01 the issue I've found with liquid types is that they are still basically dependent types and they require an SMT solver in most cases, I'm working on doing something that is decidable preferably in polynomial time  
> **username_3**: @FrancescoBertolaccini I believe that as long as you have linear arithmetic constraints in types, you can't do it in polynomial time anymore (of course, unless P=NP). Integer programming is NP-complete, so if you allow arithmetic constraints in types, they might not be solvable in polynomial time.  
> **username_3**: If you only allow the constraints of a very weak form, I suppose you can do it in polynomial time. But then you gain very little from the constraints on types.  
> **username_0**: @xuq01 Linear arithmetic is not to be allowed, I plan on only providing "bound" constraints of the type I've shown in the examples. I believe the limitedness of the language would make it restrictive, yes, but also useful in some specific applications.  
> **username_3**: @FrancescoBertolaccini Hm, I believe that you can still use the same setup. You still have Liquid Types, except that your language of constraints is highly constrained. This way you can replace the SMT solver with a built-in, less-capable solver. OTOH, if you don't have very complex constraints, maybe you're better off using symbolic execution or abstract interpretation, rather than extending the type system?  

---

## 1 answers

### Answer by username_3 on 2019-03-01. Score: 1 | Accepted answer

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

> **Comments:**
> **username_1**: Liquid types are a special case of refinement types, no?  
> **username_0**: 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.  
> **username_3**: @MartinBerger Yes, definitely. I singled them out here because IMO their presentation is clear and understandable.  

---

