4 ms·

Ada has always had integer ranges. Dependent types include integer ranges, but integer ranges aren't necessarily dependent types. Dependent types do a bit mo

Ada has always had integer ranges. Dependent types include integer ranges, but integer ranges aren't necessarily dependent types. Dependent types do a bit more than that. Supposing you want to put a random pixel on a canvas C, but you don't know C's dimensions at compile time (perhaps because the user can change them at run time). The numerical value of the pixel's x and y coordinate ranges aren't known at compile time, but it is known that they're not negative and less than C.width and C.height. C = new Canvas ... // random(n) returns an integer of type range(0, n) x = random(C.width) // x has type range(0, C.width) y = random(C.height) // y has type range(0, C.height) // drawPoint(w, j, i) takes args of type canvas, range(0, w.width), range(0, w.height). drawPoint(C, x, y) // The types of x and y depend on the run-time value of C. Using dependent typing would enable us to remove another source of bugs.

HumanDrivenDev 9y ago
> Ada has always had integer ranges. Dependent types include integer ranges, but integer ranges aren't necessarily dependent types. I was under the impression that Adas integer ranges were checked at runtime, like contracts. Is that not the case?
- DonaldFisk 9y ago
  That's correct, it's a run-time check. According to https://en.wikibooks.org/wiki/Ada_Programming/Types/range https://en.wikibooks.org/wiki/Ada_Programming/Types/range A range is a signed integer value which ranges from a First to a last Last. It is defined as range First .. Last When a value is assigned to an object with such a range constraint, the value is checked for validity and Constraint_Error exception is raised when the value is not within First to Last.
  - HumanDrivenDev 9y ago
    Right. I said dependent types would allow you to statically declare integer ranges, as is my understanding. It's interesting to me how Ada takes the approach of blending types and run time contracts. In most languages it would be two different things - a function that takes int, then a contract or assert that handles the value.
    - DonaldFisk 9y ago
      They allow you to statically declare integer ranges (as well as other things), even if their bounds are unknown until run-time, and without requiring a run-time type check.
    - mjn 9y ago
      Some Lisp implementations (like SBCL) also do that blending, although they can statically catch some integer range violations too. For example if you declare a variable to be an (integer 50 100) and try to assign a literal 30 to it, you'll get a compile-time warning in SBCL: ; Constant 30 conflicts with its asserted type (INTEGER 50 100). But in many other cases it'll generate a runtime check instead, because the static type checking is basically best-effort.

HumanDrivenDev 9y ago

> Ada has always had integer ranges. Dependent types include integer ranges, but integer ranges aren't necessarily dependent types. I was under the impression that Adas integer ranges were checked at runtime, like contracts. Is that not the case?

DonaldFisk 9y ago
That's correct, it's a run-time check. According to https://en.wikibooks.org/wiki/Ada_Programming/Types/range https://en.wikibooks.org/wiki/Ada_Programming/Types/range A range is a signed integer value which ranges from a First to a last Last. It is defined as range First .. Last When a value is assigned to an object with such a range constraint, the value is checked for validity and Constraint_Error exception is raised when the value is not within First to Last.
- HumanDrivenDev 9y ago
  Right. I said dependent types would allow you to statically declare integer ranges, as is my understanding. It's interesting to me how Ada takes the approach of blending types and run time contracts. In most languages it would be two different things - a function that takes int, then a contract or assert that handles the value.
  - DonaldFisk 9y ago
    They allow you to statically declare integer ranges (as well as other things), even if their bounds are unknown until run-time, and without requiring a run-time type check.
  - mjn 9y ago
    Some Lisp implementations (like SBCL) also do that blending, although they can statically catch some integer range violations too. For example if you declare a variable to be an (integer 50 100) and try to assign a literal 30 to it, you'll get a compile-time warning in SBCL: ; Constant 30 conflicts with its asserted type (INTEGER 50 100). But in many other cases it'll generate a runtime check instead, because the static type checking is basically best-effort.