<p>Suppose a language has a conventional list data structure that contains some dynamic number of values indexed sequentially. Some operations to access a value from the list require that a certain index exists, or that at least a certain number of values are included, and there will be an error at run time otherwise; a special case is needing just that the list be non-empty.</p>
<p>How can the language <strong>guarantee in advance that these operations will be safe, and reject any programs that would crash</strong>? What are the costs of adopting that solution?</p>
<hr />
<p>To illustrate, a couple of examples of statically <em>unsafe</em> lists in different paradigms, firstly in Java:</p>
<pre class="lang-java prettyprint-override"><code>List&lt;String&gt; l = new ArrayList&lt;String&gt;();
int i = 5;
l.get(i); // Throws IndexOutOfBoundsException at run time
</code></pre>
<p>then Haskell:</p>
<pre class="lang-haskell prettyprint-override"><code>head [] -- *** Exception: Prelude.head: empty list
</code></pre>
<p>Both of the above are typechecked and compiled without issue, but will crash at run time; in real programs, these lists would be being provided as parameters, fields, etc, and the index could be a non-literal dynamic value. Ideally, these crashing programs would be rejected statically, while programs that only retrieve items that do exist would be allowed.</p>

<types><static-typing><arrays><static-analysis><soundness>
How can a language statically ensure a required index exists in a list?
CC BY-SA 4.0
2023-06-14T03:41:13.310Z
Is this possible in the general case? What if it depends on an external value, such as user input or network data?
Bbrk24
CC BY-SA 4.0
2023-06-15T00:30:43.410Z
The sensible options include dependent types & returning an optional. Here is a silly idea to add to the list. Index using index mod size. It meets the criteria of preventing out of bounds access and retrieving only items that exist but there are some obvious correctness issues.
Bruce Adams
CC BY-SA 4.0
2023-06-27T15:33:28.743Z
@Bbrk24 of course not, you need to somehow check that the external value is in range, which must be done at runtime.
CoffeeTableEspresso
CC BY-SA 4.0
2023-08-18T16:07:39.177Z
Actually it is possible to define such a language. Dependent types do it. It just has the consequence that code where the compiler cannot prove it is rejected. Which is actually why such behavior isn't very popular.
feldentm
<h1>Dependent Types</h1>
<p>A <a href="https://en.wikipedia.org/wiki/Dependent_type" rel="nofollow noreferrer">Dependent Type</a> is one whose members can be described by a predicate <em>depending on other values</em>.<br />
In your case, it is <code>Index (xs: List a) = { i ∈ ℕ | i &lt; |xs| }</code>.<br />
As you can deduce from the <code>i ∈ ℕ</code> clause, this is a strict subtype of <code>ℕ</code>.</p>
<p>Here's an example programme description using it:</p>
<pre class="lang-hs prettyprint-override"><code>List a = enum
    Cons: a -&gt; List a -&gt; List a
    Empty: List a

length: List a -&gt; Natural
length l = f l 0 where
    f (Cons _ xs) n = f xs (n + 1)
    f Empty n = n

Index (xs: List a) = (i: Natural) when i &lt; length xs

get: (xs: List a) -&gt; Index xs -&gt; a
get (Cons x _) 0 = x
get (Cons _ xs) n = get xs (n - 1)

main = do
    let xs = Cons &quot;h&quot; (Cons &quot;42&quot; Empty)
    putStrLn (get xs 0) //ok
    putStrLn (get xs 5) //Compiler Error
</code></pre>
<p>A question that arises then is that of <code>get</code> &quot;knowing&quot; it will never get <code>Empty</code> as input, at which point one will notice that <code>length: List a -&gt; ℕ</code> has not a descriptive enough type.<br />
Indeed: <code>length</code>'s correct type is <code>(Empty -&gt; 0) &amp; (Cons -&gt; ℕ⁺)</code>, which explicitates the fact that <code>Index Empty</code> is not a type existing in the Universe.<br />
(At which point one may notice how <code>Cons</code>/<code>::</code> relates to <code>NonEmpty a</code>).<br />
How smart a language and implementation has to be to automatically understand and report on those problems then is the realm of <a href="https://en.wikipedia.org/wiki/Automated_theorem_proving" rel="nofollow noreferrer">Automated Theorem Proving</a>.</p>
<p>Naturally, when a value is not literal, one has to prove it indeed inhabits the type at hand.</p>
<pre class="lang-hs prettyprint-override"><code>let n: ℕ = userInput in
get xs n
</code></pre>
<p>is not a valid programme, for <code>ℕ</code> is a <em>supertype</em> of <code>{ i ∈ ℕ | i &lt; |xs| }</code>, meaning explicit type narrowing has to be involved:</p>
<pre class="lang-hs prettyprint-override"><code>let n: ℕ = userInput in
if n &lt; |xs| then
    get xs n
else
    //deal with error
</code></pre>
<p>which should be reminiscent of C++'s <code>dynamic_cast</code>, and is already existing practice (you don't just use unsanitised user input as-is, do you?).<br />
This also relates to the realm of <strong>Automatic Type Narrowing</strong> as featured in <a href="https://kotlinlang.org/docs/typecasts.html" rel="nofollow noreferrer">Kotlin</a>, <a href="https://www.typescriptlang.org/docs/handbook/2/narrowing.html" rel="nofollow noreferrer">TypeScript</a>, and, less automatic, <a href="http://web.archive.org/web/20211129230702/https://ceylon-lang.org/documentation/1.3/tour/types/#narrowing_the_type_of_an_object_reference" rel="nofollow noreferrer">Ceylon</a>.</p>
<p>An other example is that of <code>Min</code> and <code>Max</code>: <code>∀(a: Comparable). MinMax (x: a, y: a) = { x, y }</code>, which may be used to describe functions such as</p>
<pre class="lang-hs prettyprint-override"><code>MinMax = ∀a. Comparable a =&gt; (x: a) -&gt; (y: a) -&gt; (x | y)

max: MinMax
max x y = if x &gt; y then x else y

min: MinMax
min x y = if x &gt; y then y else x
</code></pre>
<p>where <code>x</code> and <code>y</code> are runtime values used as <a href="https://languagedesign.stackexchange.com/a/1540/504">singleton types</a> in a <a href="https://en.wikipedia.org/wiki/Union_type" rel="nofollow noreferrer">union type</a>, where it is guaranteed that for each pair of <code>x</code> and <code>y</code>, <code>min</code> and <code>max</code> both will return <em>precisely</em> either that <code>x</code> or that <code>y</code>, <em>and nothing else</em>.<br />
Naturally the result of <code>min</code> and <code>max</code> is a strict subset of <code>a</code> by virtue of <code>{ x ∈ a | f(x) } &lt;: a</code>.</p>
<p>Languages implementing those include, among others, <a href="https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#dependent-types" rel="nofollow noreferrer">Idris</a>, <a href="https://agda.readthedocs.io/en/latest/language/function-definitions.html#function-definitions" rel="nofollow noreferrer">Agda</a>, Coq, F*, and <a href="https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/c2243.html" rel="nofollow noreferrer">ATS</a>.</p>

CC BY-SA 4.0
2023-06-14T04:25:05.917Z
2023-06-27T00:55:11.200Z
2023-06-27T00:55:11.200Z
Longinus
CC BY-SA 4.0
2023-07-11T19:49:32.283Z
In what language are the code examples written? I see that they are marked as Haskell, but they look similar to Haskell but not the same.
user570286
CC BY-SA 4.0
2023-07-11T23:06:27.063Z
@user570286 Pseudo-code I made up. `when` in types should be reminiscent of LiquidHaskell, and the `enum` types are GADTs
Longinus
CC BY-SA 4.0
2023-07-11T23:11:06.993Z
@user570286 Also [Raku](https://docs.raku.org/language/typesystem#subset) because of course Raku supports this.
Longinus
<p>Let's get the easy solution out of the way first: you can just have these operations like <code>get(int)</code> and <code>head()</code> return an <a href="https://en.wikipedia.org/wiki/Option_type" rel="nofollow noreferrer">optional value</a>, and then it's statically checked that you handle both cases where the element does or doesn't exist, the same way it's checked for an option type. Some notable languages which do this are <a href="https://doc.rust-lang.org/std/slice/trait.SliceIndex.html#tymethod.get" rel="nofollow noreferrer">Rust</a> (<code>get</code>), <a href="https://v2.ocaml.org/api/List.html" rel="nofollow noreferrer">OCaml</a> (<code>nth_opt</code>) and <a href="https://fsharp.github.io/fsharp-core-docs/reference/fsharp-collections-listmodule.html#tryItem" rel="nofollow noreferrer">F#</a> (<code>tryItem</code>).</p>
<p>It's perhaps a bit cumbersome to force the user to handle an option every time they use a fundamental list operation; but in practice it's often not that big a deal, because most of the time you want to access the elements in a list, you do so through an iterator rather than the <code>get</code> method directly.</p>
<hr />
<p>Other solutions could be based on theorem-proving; the goal is to statically prove that 0 ≤ <em>i</em> &lt; <em>n</em> as a precondition for calling <code>get(i)</code>, and reject the method call if this precondition can't be proved. There are different ways of going about this:</p>
<ul>
<li>You can include a sub-language in which the programmer can state and prove such propositions; normally, this is based on <a href="https://en.wikipedia.org/wiki/Hoare_logic" rel="nofollow noreferrer">Hoare logic</a> or a similar logic. This approach gives languages like <a href="https://en.wikipedia.org/wiki/F*_(programming_language)" rel="nofollow noreferrer">F*</a> or tools like <a href="https://en.wikipedia.org/wiki/KeY" rel="nofollow noreferrer">KeY</a>.</li>
<li>You can have the compiler try to automatically prove them based on the conditions in branching statements; this would be something like control-flow type narrowing with dependent types. I don't know if any existing languages do this.</li>
</ul>
<p>See also: <a href="https://languagedesign.stackexchange.com/q/1436/89">What options are there for adding formal verification to a general purpose programming language?</a></p>

CC BY-SA 4.0
2023-06-14T04:10:09.283Z
2023-06-15T21:05:19.893Z
2023-06-15T21:05:19.893Z
kaya3
CC BY-SA 4.0
2023-06-14T04:27:58.203Z
I think I've heard of a language that uses *integer range types* in one of Discord PL communities. Ranges can be inferred on arithmetic operations as well as branches, so it could fill in the "automatic proof" category.
Bubbler
<h2>A <code>MimimumLengthList&lt;int&gt;</code>/<code>MaximumValueInteger&lt;int&gt;</code> trait</h2>
<p><em>I think this is basically the same as dependent types but maybe easier to understand</em></p>
<p>The operation <code>a[5]</code> requires <code>a: MimimumLengthList&lt;6&gt;</code>. There are a few ways to get a <code>MimimumLengthList</code>:</p>
<ol>
<li>The list has a known size</li>
</ol>
<pre><code>list: a[6] = [1,2,3,4,5,6];
a[5]; // Ok
</code></pre>
<ol start="2">
<li>You assert the list is a mimimum length list:</li>
</ol>
<pre><code>fn f(a: MimimumLengthList&lt;6&gt;) { return a[5]; //ok }
</code></pre>
<ol start="3">
<li>An explicit check</li>
</ol>
<pre><code>let a = json_parse(input());
if (a.len() &gt; 5)  {// this is a type assertion, special cased by the type checker
    return a[5];
}
</code></pre>
<p>Last case is similar to what languages that check bounds at runtime would do, but now you need to explicitly check and can choose other actions to perform in the false case besides just throwing an error.</p>
<h3>Maximum Value Integer</h3>
<p>You may sometimes want to do:</p>
<pre><code>x: int = input();
if (x&lt;5) {
    print([1,2,3,4,5][x]);
}
</code></pre>
<p>For this purpose, you can make a trait <code>MaximumValueInteger</code> which just represents an integer asserted to be less than a given value.</p>
<h3>Combining the two</h3>
<p>You could safely define a function like this:</p>
<pre><code>fn get(a: MinimumLengthList&lt;5&gt;, b:MaximumValueInteger&lt;4&gt;){a[b]}
a([1,2,3,4,5,6,7,8], 2);
</code></pre>
<p>However, conditionals get a bit more complex:&quot;</p>
<pre><code>if (a &lt; len(b)) {
    b[a]
}
</code></pre>
<p>In this case, it's hard for the type checker to actually assert what type <code>a</code> and <code>b</code> is since neither of them is known at compile time. Yet both are safe. You could implement this as a kind of generic only during the type checker phase, something like:</p>
<pre><code>if (a &lt; len(b))&lt;T&gt;: a:MaximumSizeInteger&lt;T&gt;, b:MimimumLengthList&lt;T&gt; {
     
}
</code></pre>
<p>I made up syntax for conditional type assertion here since I'm not aware of any languages that have it.</p>

CC BY-SA 4.0
2023-06-14T05:18:54.857Z
2023-06-14T05:18:54.857Z
mousetail 'he-him'
# How can a language statically ensure a required index exists in a list?
Posted by: username_0 on 2023-06-14
Suppose a language has a conventional list data structure that contains some dynamic number of values indexed sequentially. Some operations to access a value from the list require that a certain index exists, or that at least a certain number of values are included, and there will be an error at run time otherwise; a special case is needing just that the list be non-empty.
How can the language guarantee in advance that these operations will be safe, and reject any programs that would crash? What are the costs of adopting that solution?

To illustrate, a couple of examples of statically unsafe lists in different paradigms, firstly in Java:
List l = new ArrayList();
int i = 5;
l.get(i); // Throws IndexOutOfBoundsException at run time

then Haskell:
head [] -- *** Exception: Prelude.head: empty list

Both of the above are typechecked and compiled without issue, but will crash at run time; in real programs, these lists would be being provided as parameters, fields, etc, and the index could be a non-literal dynamic value. Ideally, these crashing programs would be rejected statically, while programs that only retrieve items that do exist would be allowed.
**Tags:** types static-typing arrays static-analysis soundness
> **Comments:**
> **username_1**: Is this possible in the general case? What if it depends on an external value, such as user input or network data?  
> **username_2**: The sensible options include dependent types & returning an optional. Here is a silly idea to add to the list. Index using index mod size. It meets the criteria of preventing out of bounds access and retrieving only items that exist but there are some obvious correctness issues.  
> **username_3**: @Bbrk24 of course not, you need to somehow check that the external value is in range, which must be done at runtime.  
> **username_4**: Actually it is possible to define such a language. Dependent types do it. It just has the consequence that code where the compiler cannot prove it is rejected. Which is actually why such behavior isn't very popular.  
---
## 3 answers
### Answer by username_5 on 2023-06-14. Score: 9
Dependent Types
A Dependent Type is one whose members can be described by a predicate depending on other values.
In your case, it is Index (xs: List a) = { i ∈ ℕ | i < |xs| }.
As you can deduce from the i ∈ ℕ clause, this is a strict subtype of ℕ.
Here's an example programme description using it:
List a = enum
    Cons: a -> List a -> List a
    Empty: List a

length: List a -> Natural
length l = f l 0 where
    f (Cons _ xs) n = f xs (n + 1)
    f Empty n = n

Index (xs: List a) = (i: Natural) when i < length xs

get: (xs: List a) -> Index xs -> a
get (Cons x _) 0 = x
get (Cons _ xs) n = get xs (n - 1)

main = do
    let xs = Cons "h" (Cons "42" Empty)
    putStrLn (get xs 0) //ok
    putStrLn (get xs 5) //Compiler Error

A question that arises then is that of get "knowing" it will never get Empty as input, at which point one will notice that length: List a -> ℕ has not a descriptive enough type.
Indeed: length's correct type is (Empty -> 0) & (Cons -> ℕ⁺), which explicitates the fact that Index Empty is not a type existing in the Universe.
(At which point one may notice how Cons/:: relates to NonEmpty a).
How smart a language and implementation has to be to automatically understand and report on those problems then is the realm of Automated Theorem Proving.
Naturally, when a value is not literal, one has to prove it indeed inhabits the type at hand.
let n: ℕ = userInput in
get xs n

is not a valid programme, for ℕ is a supertype of { i ∈ ℕ | i < |xs| }, meaning explicit type narrowing has to be involved:
let n: ℕ = userInput in
if n < |xs| then
    get xs n
else
    //deal with error

which should be reminiscent of C++'s dynamic_cast, and is already existing practice (you don't just use unsanitised user input as-is, do you?).
This also relates to the realm of Automatic Type Narrowing as featured in Kotlin, TypeScript, and, less automatic, Ceylon.
An other example is that of Min and Max: ∀(a: Comparable). MinMax (x: a, y: a) = { x, y }, which may be used to describe functions such as
MinMax = ∀a. Comparable a => (x: a) -> (y: a) -> (x | y)

max: MinMax
max x y = if x > y then x else y

min: MinMax
min x y = if x > y then y else x

where x and y are runtime values used as singleton types in a union type, where it is guaranteed that for each pair of x and y, min and max both will return precisely either that x or that y, and nothing else.
Naturally the result of min and max is a strict subset of a by virtue of { x ∈ a | f(x) } <: a.
Languages implementing those include, among others, Idris, Agda, Coq, F*, and ATS.
> **Comments:**
> **username_6** (2023-07-11): In what language are the code examples written? I see that they are marked as Haskell, but they look similar to Haskell but not the same.  
> **username_5** (2023-07-11): @user570286 Pseudo-code I made up. `when` in types should be reminiscent of LiquidHaskell, and the `enum` types are GADTs  
> **username_5** (2023-07-11): @user570286 Also [Raku](https://docs.raku.org/language/typesystem#subset) because of course Raku supports this.  
---
### Answer by username_7 on 2023-06-14. Score: 4
Let's get the easy solution out of the way first: you can just have these operations like `get(int)` and `head()` return an [optional value](https://en.wikipedia.org/wiki/Option_type), and then it's statically checked that you handle both cases where the element does or doesn't exist, the same way it's checked for an option type. Some notable languages which do this are [Rust](https://doc.rust-lang.org/std/slice/trait.SliceIndex.html#tymethod.get) (`get`), [OCaml](https://v2.ocaml.org/api/List.html) (`nth_opt`) and [F#](https://fsharp.github.io/fsharp-core-docs/reference/fsharp-collections-listmodule.html#tryItem) (`tryItem`).

It's perhaps a bit cumbersome to force the user to handle an option every time they use a fundamental list operation; but in practice it's often not that big a deal, because most of the time you want to access the elements in a list, you do so through an iterator rather than the `get` method directly.

---

Other solutions could be based on theorem-proving; the goal is to statically prove that 0 ≤ *i* < *n* as a precondition for calling `get(i)`, and reject the method call if this precondition can't be proved. There are different ways of going about this:

* You can include a sub-language in which the programmer can state and prove such propositions; normally, this is based on [Hoare logic](https://en.wikipedia.org/wiki/Hoare_logic) or a similar logic. This approach gives languages like [F\*](https://en.wikipedia.org/wiki/F*_(programming_language)) or tools like [KeY](https://en.wikipedia.org/wiki/KeY).
* You can have the compiler try to automatically prove them based on the conditions in branching statements; this would be something like control-flow type narrowing with dependent types. I don't know if any existing languages do this.

See also: [What options are there for adding formal verification to a general purpose programming language?](https://languagedesign.stackexchange.com/q/1436/89)
> **Comments:**
> **username_8** (2023-06-14): I think I've heard of a language that uses *integer range types* in one of Discord PL communities. Ranges can be inferred on arithmetic operations as well as branches, so it could fill in the "automatic proof" category.  
---
### Answer by username_9 on 2023-06-14. Score: 3
A MimimumLengthList/MaximumValueInteger trait
I think this is basically the same as dependent types but maybe easier to understand
The operation a[5] requires a: MimimumLengthList<6>. There are a few ways to get a MimimumLengthList:

The list has a known size

list: a[6] = [1,2,3,4,5,6];
a[5]; // Ok


You assert the list is a mimimum length list:

fn f(a: MimimumLengthList<6>) { return a[5]; //ok }


An explicit check

let a = json_parse(input());
if (a.len() > 5)  {// this is a type assertion, special cased by the type checker
    return a[5];
}

Last case is similar to what languages that check bounds at runtime would do, but now you need to explicitly check and can choose other actions to perform in the false case besides just throwing an error.
Maximum Value Integer
You may sometimes want to do:
x: int = input();
if (x<5) {
    print([1,2,3,4,5][x]);
}

For this purpose, you can make a trait MaximumValueInteger which just represents an integer asserted to be less than a given value.
Combining the two
You could safely define a function like this:
fn get(a: MinimumLengthList<5>, b:MaximumValueInteger<4>){a[b]}
a([1,2,3,4,5,6,7,8], 2);

However, conditionals get a bit more complex:"
if (a < len(b)) {
    b[a]
}

In this case, it's hard for the type checker to actually assert what type a and b is since neither of them is known at compile time. Yet both are safe. You could implement this as a kind of generic only during the type checker phase, something like:
if (a < len(b)): a:MaximumSizeInteger, b:MimimumLengthList {
     
}

I made up syntax for conditional type assertion here since I'm not aware of any languages that have it.
---
