<p>Rust is famous for its ownership type-system, but requires the programmer to annotate ownership in function signatures. Is it possible to do full program inference of ownership, without any annotations? What would be the pros and cons of such a system?</p>

CC BY-SA 4.0
2020-06-29T16:41:36.977Z
The term you might be looking for is *partial type inference*. The reason why many languages don't have full type inference is that once you go beyond Hindley/Milner let-polymorphism, full type inference is generally undecidable.
Martin Berger
CC BY-SA 4.0
2020-06-29T18:24:55.193Z
@MartinBerger No. Rust already has partial inference. This question is about full inference.
Olle Härstedt
CC BY-SA 4.0
2020-06-29T19:19:40.293Z
I know that Rust has partial type inference. I was just clarifying terminology.
Martin Berger
CC BY-SA 4.0
2020-07-01T08:51:11.223Z
As a general rule of thumb, any dynamic feature of a langauge (ownership at runtime, effects, shape of heap, what is printed out) can only be *approximated* by a type system that has algorithmic checking or inference, because questions about the dynamic behavior of programs get undecidable really fast. One always ends up balancing expressivity and simplicity.
Andrej Bauer
CC BY-SA 4.0
2020-07-04T11:08:42.163Z
@OlleHärstedt what Andrej said is formalised in the famous [Rice's Theorem](https://en.wikipedia.org/wiki/Rice%27s_theorem).
Martin Berger
CC BY-SA 4.0
2020-07-04T12:16:25.813Z
Sure, but that still leaves out the question if ownership inference is usable, even if you end up with the ownership type `any` in some cases.
Olle Härstedt
CC BY-SA 4.0
2020-07-04T14:46:07.820Z
@OlleHärstedt Please clarify what you mean by "full ownership inference", as                                             
this is unclear. Maybe something like this: given a type-erasure                                                
function $ter(\cdot)$ which removes all type annotations from Rust                                              
programs (so the result is not, technically Rust). Let's call _Rust--_                                          
the set of all programs $ter(P)$ where $P$ is a syntactically valid                                             
Rust program. (1/3)
Martin Berger
CC BY-SA 4.0
2020-07-04T14:46:27.557Z
The question you seem to be asking is this: is there an                                           
algorithm $ti(\cdot)$ such that for all _Rust--_ programs $M$, $ti(M)                                           
= (\Gamma, t)$ exactly when there is a Rust program $P$, typable as                                             
$\Gamma' \vdash P : t'$, and then:  $ter(P) = M$, as well as:                                              
$(\Gamma', t')$ is a generalisation of $(\Gamma, t)$. (2/3)
Martin Berger
CC BY-SA 4.0
2020-07-04T14:46:46.220Z
I'm leaving                                             
open, what exactly generalisation means, there are several possible                                             
interpretations, you need to clarify what you have in mind.    (3/3)
Martin Berger
<type-theory>
Is full ownership inference possible?
Olle Härstedt
# Is full ownership inference possible?

(Asked by: username_0 on 2020-06-27)

Rust is famous for its ownership type-system, but requires the programmer to annotate ownership in function signatures. Is it possible to do full program inference of ownership, without any annotations? What would be the pros and cons of such a system?

**Tags:** type-theory
> **Comments:**
> **username_1**: The term you might be looking for is *partial type inference*. The reason why many languages don't have full type inference is that once you go beyond Hindley/Milner let-polymorphism, full type inference is generally undecidable.  
> **username_0**: @MartinBerger No. Rust already has partial inference. This question is about full inference.  
> **username_1**: I know that Rust has partial type inference. I was just clarifying terminology.  
> **username_2**: As a general rule of thumb, any dynamic feature of a langauge (ownership at runtime, effects, shape of heap, what is printed out) can only be *approximated* by a type system that has algorithmic checking or inference, because questions about the dynamic behavior of programs get undecidable really fast. One always ends up balancing expressivity and simplicity.  
> **username_1**: @OlleHärstedt what Andrej said is formalised in the famous [Rice's Theorem](https://en.wikipedia.org/wiki/Rice%27s_theorem).  
> **username_0**: Sure, but that still leaves out the question if ownership inference is usable, even if you end up with the ownership type `any` in some cases.  
> **username_1**: @OlleHärstedt Please clarify what you mean by "full ownership inference", as                                              this is unclear. Maybe something like this: given a type-erasure                                                 function $ter(\cdot)$ which removes all type annotations from Rust                                               programs (so the result is not, technically Rust). Let's call _Rust--_                                           the set of all programs $ter(P)$ where $P$ is a syntactically valid                                              Rust program. (1/3)  
> **username_1**: The question you seem to be asking is this: is there an                                            algorithm $ti(\cdot)$ such that for all _Rust--_ programs $M$, $ti(M)                                            = (\Gamma, t)$ exactly when there is a Rust program $P$, typable as                                              $\Gamma' \vdash P : t'$, and then:  $ter(P) = M$, as well as:                                               $(\Gamma', t')$ is a generalisation of $(\Gamma, t)$. (2/3)  
> **username_1**: I'm leaving                                              open, what exactly generalisation means, there are several possible                                              interpretations, you need to clarify what you have in mind.    (3/3)  

---

## 0 answers

