2 ms·

Julia has Value types for when a primitive type can be used during compilation: https://docs.julialang.org/en/v1.10/manual/types/#%22Value-types%22 https://docs

Julia has Value types for when a primitive type can be used during compilation: https://docs.julialang.org/en/v1.10/manual/types/#%22Value-types%22 https://docs.julialang.org/en/v1.10/manual/types/#%22Value-t... They aren't the same thing, I mostly brought them up to point out that Ada can only throw compile-time errors for range types under limited circumstances, otherwise you're expressing a runtime bounds check using the type system. Which I agree is a nice feature for a static language, which Julia is not; Ada won't let you leave out the runtime check, so numbers outside the range are unrepresentable in the program. It should be possible to use Value types to write a generated function which instantiates a constructor for a primitive type which is restricted to a range. All type errors in Julia are at runtime, but like I said, Ada has to push many range exceptions to runtime as well, and the property that a number outside of the range is unrepresentable is preserved in both cases. Although I can't point you at an implementation of this in Julia, I'm increasingly confident that it could be done. Julia's type system is also powerful enough to express units https://github.com/PainterQubits/Unitful.jl https://github.com/PainterQubits/Unitful.jl

kevlar700 3y ago
Ada is very flexible and does let you leave out the runtime check. However the program will be stopped or atleast be exceptive by default if a logic error creates an invalid value that you haven't checked the validity of. Spark can be used for a higher degree of value analysis at compile time because flow analysis is obviously needed in many cases. Volatility can still be an issue but in most cases Ada knows the inputs such as for API usage validity.
- samatman 3y ago
  I would rather say that Ada allows you to remove the runtime check on ranges. This is the opposite of enforcing a range with a home-rolled check of the values, that's what I mean by "won't let you leave it out": without deliberate action, the range will either be proven by static analysis to be in-bounds, or that invariant will be checked at runtime. Julia has a similar system for array bounds: by default, accessing an array is checked for range restriction, and an error is thrown if the value is out of range. Range checks inside functions (including the system `getindex` function) can be annotated with the @boundscheck macro, and user code which knows an index is in-range can use @inbounds to elide that check. If this is done wrong, Julia will segfault or corrupt memory. In C, if it isn't all done perfectly correctly, same thing: opt-in, not opt-out. Julia is more like Ada in that respect.

kevlar700 3y ago

Ada is very flexible and does let you leave out the runtime check. However the program will be stopped or atleast be exceptive by default if a logic error creates an invalid value that you haven't checked the validity of. Spark can be used for a higher degree of value analysis at compile time because flow analysis is obviously needed in many cases. Volatility can still be an issue but in most cases Ada knows the inputs such as for API usage validity.

samatman 3y ago
I would rather say that Ada allows you to remove the runtime check on ranges. This is the opposite of enforcing a range with a home-rolled check of the values, that's what I mean by "won't let you leave it out": without deliberate action, the range will either be proven by static analysis to be in-bounds, or that invariant will be checked at runtime. Julia has a similar system for array bounds: by default, accessing an array is checked for range restriction, and an error is thrown if the value is out of range. Range checks inside functions (including the system `getindex` function) can be annotated with the @boundscheck macro, and user code which knows an index is in-range can use @inbounds to elide that check. If this is done wrong, Julia will segfault or corrupt memory. In C, if it isn't all done perfectly correctly, same thing: opt-in, not opt-out. Julia is more like Ada in that respect.