<p><strong>Context</strong></p>
<p>For memory safe languages to be fast, array bounds should be checked during compilation. Some language like Java, Rust, Swift, and others eliminate array bounds checks <em>when possible</em>, but the developer often can't tell for sure when.</p>
<p>The Wikipedia article about <a href="https://en.wikipedia.org/wiki/Dependent_type" rel="noreferrer">dependent types</a> states &quot;a dependent pair may be used to pair an array with its length in a type-safe way&quot;. However I didn't find any general purpose languages that use dependent types for array bound checks. I'm aware of the <a href="https://skia.googlesource.com/external/github.com/google/wuffs/+/HEAD/doc/wuffs-the-language.md" rel="noreferrer">Wuffs</a> language, but it doesn't use dependent types.</p>
<p>There is <a href="https://www.cs.cmu.edu/%7Efp/papers/pldi98dml.pdf" rel="noreferrer">research</a> in this area on the effectiveness of this approach.</p>
<p><strong>Example Syntax</strong></p>
<p>The question is not &quot;what is the best syntax&quot;, but still, to illustrate and provide a concrete example, so that we don't have to talk in a too abstract way, which can lead to misunderstanding. Access without runtime checks require that the compiler verifies correctness. Index variables with range restrictions allow this. The conditional <code>break</code> guarantees that <code>i</code> is within the bounds.</p>
<pre><code>// proof the array is not empty
if data.len &gt; 0
    // set i to 0 (which is in-bound given the above proof)
    // and define a dependent type that is in-bound
    i := 0..data.len
    while true
        // array access, guaranteed without bound checks
        data[i]! = i
        // proof we can increment
        if i &gt;= data.len - 1
            break
        i += 1
</code></pre>
<p><strong>Questions</strong></p>
<p>I'm mostly interested in the <a href="https://langdev.stackexchange.com/help/on-topic">history</a> (if there is any) and research in this area.</p>
<p>Dependent types can avoid the need for run-time bounds checks by making that information statically-determined, or propagating the result of an earlier dynamic (explicit) check. Used for this limited purpose, they could be simpler than general dependent types. What are the origins and history (if any) of limited-purpose dependent types only for array bounds in programming languages?</p>

<arrays><history><memory-safety><dependent-types>
What is the history of using dependent types to avoid array bound checks
CC BY-SA 4.0
2024-07-01T08:32:46.353Z
The title of this question is asking whether dependent types are good for a specific purpose, and then the second half of the body is all about syntax; what is it intending to be about? The question right at the end is extraordinarily broad and seems to be seeking ideation; this may not be a good fit for an answerable question here.
Michael Homer
CC BY-SA 4.0
2024-07-01T08:34:28.747Z
if you have dependent types i think a better approach is to require that indices are _always_ accompanied by a bounds-check proof and let the user write if (oob) panic as needed to produce such proofs if they really want
Moonchild
CC BY-SA 4.0
2024-07-01T08:35:29.310Z
It may be useful to look in the [help/on-topic] for an idea of the sorts of question format that do & don't fit - it gives some high-level guidance as well as linking to some meta posts discussing different areas.
Michael Homer
CC BY-SA 4.0
2024-07-01T08:36:39.080Z
The syntax example should give a concrete example on how this could look like (the syntax is not part of the question, but to give context). I'm looking for feedback from practical experience, if there is any. I'm not sure how to phrase it in a better way, I'm sorry.
Thomas Mueller
CC BY-SA 4.0
2024-07-01T08:40:36.753Z
@Moonchild the syntax example does provide the proofs: `if data.len` requires that we do not have an empty array.  `i := 0..data.len` sets it to 0 initially (which is possible with the previous proof), and tells the compiler that the maximum value is `data.len - 1`. The conditional `break i >= data.len - 1` garantees that we can increment without violating the bounds.
Thomas Mueller
CC BY-SA 4.0
2024-07-01T08:47:49.103Z
@MichaelHomer I guess I'm "[explicitly seeking empirical evidence](https://langdev.meta.stackexchange.com/questions/578/are-what-are-some-possible-syntaxes-questions-on-topic)", and possible "[history](https://langdev.stackexchange.com/questions/tagged/history)" (if there is any).
Thomas Mueller
CC BY-SA 4.0
2024-07-01T08:58:09.867Z
@ThomasMueller i'm saying there should be one syntax and it should always require bounds proofs
Moonchild
CC BY-SA 4.0
2024-07-01T09:02:33.893Z
@Moonchild OK I understand! I had in mind two syntaxes: one (the default) that has no proof and so does array bound checks; and a second syntax that comes with proofs. But I understand now what you mean!
Thomas Mueller
CC BY-SA 4.0
2024-07-01T09:12:39.387Z
The help centre items suggest some structures that can guide the shape of questions — they're not just incantations to be invoked — so a question would be built to be clear what sort of information it was looking for and how it would be possible to judge whether the answers were correct, rather than a tag on the end, and realistically it won't be able to cover multiple broad areas. A history question about the development of accepted syntaxes for a construction would be ok, but even after the edits I'm not sure exactly *which* thing it's looking for instances of. I don't see any empirical part
Michael Homer
CC BY-SA 4.0
2024-07-01T09:21:26.127Z
Is this a reflection of the question you're aiming for? "Dependent types can avoid the need for run-time bounds checks by making that information statically-determined, or propagating the result of an earlier dynamic check. Used for this limited purpose, they could be simpler than general dependent types. What are the origins and history of limited-purpose dependent types only for array bounds in programming languages?" - I'm not sure whether that helps with your overall goal or not but it is probably a valid [tag:history] question, although it'd be better to have an attested instance to trace
Michael Homer
CC BY-SA 4.0
2024-07-01T09:22:46.690Z
An empirical question could look for human-factors research on ease of use, or perhaps ecosystem studies on defect rates and the like — I'm not sure that any exist, though that wouldn't invalidate it as a question.
Michael Homer
CC BY-SA 4.0
2024-07-01T09:50:24.500Z
@MichaelHomer Exactly! I have updated the question.
Thomas Mueller
CC BY-SA 4.0
2024-07-01T19:57:35.203Z
To be clear, it’s one or the other, not both, so this question is still unfocused. The history and empirical question are different questions with different, *incomparable* answers — that’s what makes it a problem for the format. It’s also important to identify empirical evidence *of what*, since otherwise that’d also be very broad and likely lead to answers that don’t touch your underlying question in many cases.
Michael Homer
CC BY-SA 4.0
2024-07-01T20:29:13.527Z
@MichaelHomer i have updated the question
Thomas Mueller
CC BY-SA 4.0
2024-07-02T17:41:36.997Z
I think the question is wrong in that it confuses type checks with optimization. The type part would somehow imply a semantic difference. However, the question is phrased as if that would not be the case. Is it meant to be equivalent to "what languages with mandatory range checks have optimizations to get rid of them? (including history thereof)"?
feldentm
CC BY-SA 4.0
2024-07-03T14:43:02.420Z
@feldentm I'm aware of the 'regular' ways that compilers use to avoid bound checks. However I'm specifically interested in using dependent types. Because I believe this will allow the compiler to avoid more checks (granted: by putting more burden on the developer). Specially for library functions. Also, using a special syntax for "range checked access" gives the developer more insight in which array accesses do not have checks, which is important when optimizing for performance. So, I don't think the question is "wrong".
Thomas Mueller
# What is the history of using dependent types to avoid array bound checks
Posted by: username_0 on 2024-07-01
Context
For memory safe languages to be fast, array bounds should be checked during compilation. Some language like Java, Rust, Swift, and others eliminate array bounds checks when possible, but the developer often can't tell for sure when.
The Wikipedia article about dependent types states "a dependent pair may be used to pair an array with its length in a type-safe way". However I didn't find any general purpose languages that use dependent types for array bound checks. I'm aware of the Wuffs language, but it doesn't use dependent types.
There is research in this area on the effectiveness of this approach.
Example Syntax
The question is not "what is the best syntax", but still, to illustrate and provide a concrete example, so that we don't have to talk in a too abstract way, which can lead to misunderstanding. Access without runtime checks require that the compiler verifies correctness. Index variables with range restrictions allow this. The conditional break guarantees that i is within the bounds.
// proof the array is not empty
if data.len > 0
    // set i to 0 (which is in-bound given the above proof)
    // and define a dependent type that is in-bound
    i := 0..data.len
    while true
        // array access, guaranteed without bound checks
        data[i]! = i
        // proof we can increment
        if i >= data.len - 1
            break
        i += 1

Questions
I'm mostly interested in the history (if there is any) and research in this area.
Dependent types can avoid the need for run-time bounds checks by making that information statically-determined, or propagating the result of an earlier dynamic (explicit) check. Used for this limited purpose, they could be simpler than general dependent types. What are the origins and history (if any) of limited-purpose dependent types only for array bounds in programming languages?
**Tags:** arrays history memory-safety dependent-types
> **Comments:**
> **username_1**: The title of this question is asking whether dependent types are good for a specific purpose, and then the second half of the body is all about syntax; what is it intending to be about? The question right at the end is extraordinarily broad and seems to be seeking ideation; this may not be a good fit for an answerable question here.  
> **username_2**: if you have dependent types i think a better approach is to require that indices are _always_ accompanied by a bounds-check proof and let the user write if (oob) panic as needed to produce such proofs if they really want  
> **username_1**: It may be useful to look in the [help/on-topic] for an idea of the sorts of question format that do & don't fit - it gives some high-level guidance as well as linking to some meta posts discussing different areas.  
> **username_0**: The syntax example should give a concrete example on how this could look like (the syntax is not part of the question, but to give context). I'm looking for feedback from practical experience, if there is any. I'm not sure how to phrase it in a better way, I'm sorry.  
> **username_0**: @Moonchild the syntax example does provide the proofs: `if data.len` requires that we do not have an empty array.  `i := 0..data.len` sets it to 0 initially (which is possible with the previous proof), and tells the compiler that the maximum value is `data.len - 1`. The conditional `break i >= data.len - 1` garantees that we can increment without violating the bounds.  
> **username_0**: @MichaelHomer I guess I'm "[explicitly seeking empirical evidence](https://langdev.meta.stackexchange.com/questions/578/are-what-are-some-possible-syntaxes-questions-on-topic)", and possible "[history](https://langdev.stackexchange.com/questions/tagged/history)" (if there is any).  
> **username_2**: @ThomasMueller i'm saying there should be one syntax and it should always require bounds proofs  
> **username_0**: @Moonchild OK I understand! I had in mind two syntaxes: one (the default) that has no proof and so does array bound checks; and a second syntax that comes with proofs. But I understand now what you mean!  
> **username_1**: The help centre items suggest some structures that can guide the shape of questions — they're not just incantations to be invoked — so a question would be built to be clear what sort of information it was looking for and how it would be possible to judge whether the answers were correct, rather than a tag on the end, and realistically it won't be able to cover multiple broad areas. A history question about the development of accepted syntaxes for a construction would be ok, but even after the edits I'm not sure exactly *which* thing it's looking for instances of. I don't see any empirical part  
> **username_1**: Is this a reflection of the question you're aiming for? "Dependent types can avoid the need for run-time bounds checks by making that information statically-determined, or propagating the result of an earlier dynamic check. Used for this limited purpose, they could be simpler than general dependent types. What are the origins and history of limited-purpose dependent types only for array bounds in programming languages?" - I'm not sure whether that helps with your overall goal or not but it is probably a valid [tag:history] question, although it'd be better to have an attested instance to trace  
> **username_1**: An empirical question could look for human-factors research on ease of use, or perhaps ecosystem studies on defect rates and the like — I'm not sure that any exist, though that wouldn't invalidate it as a question.  
> **username_0**: @MichaelHomer Exactly! I have updated the question.  
> **username_1**: To be clear, it’s one or the other, not both, so this question is still unfocused. The history and empirical question are different questions with different, *incomparable* answers — that’s what makes it a problem for the format. It’s also important to identify empirical evidence *of what*, since otherwise that’d also be very broad and likely lead to answers that don’t touch your underlying question in many cases.  
> **username_0**: @MichaelHomer i have updated the question  
> **username_3**: I think the question is wrong in that it confuses type checks with optimization. The type part would somehow imply a semantic difference. However, the question is phrased as if that would not be the case. Is it meant to be equivalent to "what languages with mandatory range checks have optimizations to get rid of them? (including history thereof)"?  
> **username_0**: @feldentm I'm aware of the 'regular' ways that compilers use to avoid bound checks. However I'm specifically interested in using dependent types. Because I believe this will allow the compiler to avoid more checks (granted: by putting more burden on the developer). Specially for library functions. Also, using a special syntax for "range checked access" gives the developer more insight in which array accesses do not have checks, which is important when optimizing for performance. So, I don't think the question is "wrong".  
---
## 0 answers
