6 ms·

> What kind of safety theorem should I be looking for? I mean, what I generally want is something like "if an expression of type A evaluates, the result will be

> What kind of safety theorem should I be looking for? I mean, what I generally want is something like "if an expression of type A evaluates, the result will be a valid thing of type A i.e. a value constructed by one of the constructors I defined for values of type A". This is probably sufficient for a Coq-style proof assistant, but from a general-purpose programming language I expect more. See below. > I kind of want a "the system will never magic up an A out of nowhere" result, but AIUI I can never get that because I can't have a proof of consistency of the system, no? A type system can and should guarantee that you can't create values of a (positive) type other than by using the type's introuction forms. > What is it that we can't do currently? (0) The obvious: Be sure your program won't attempt to read from or write to a close file. (1) Obtain an arbitrary integer `n`. Test once whether it is a valid array index. If the test succeeds, use `n` arbitrarily often as an array index, without any further bounds-checking. (2) Obtain three `foo.Index` values `a,b,c`. Test once whether the arrays `foo` and `bar` have the same length. Use `a,b,c` arbitrarily often as values of type `bar.Index`, without any further bounds-checking. etc. etc. etc. > The only way I can see for a type to ever get into code, in any language, is either through a literal or a cast, and both those approaches are open to me in Scala. Are those casts safe without runtime checks? --- In any case, at some point using types for program verification offers diminishing returns. We have to accept the possibility that maybe it's us, not type checkers, who have to verify our programs.

lmm 9y ago
> (0) The obvious: Be sure your program won't attempt to read from or write to a close file. I can do that in Scala with monadic regions, which only need existentials/rank-2 types. > (1) Obtain an arbitrary integer `n`. Test once whether it is a valid array index. If the test succeeds, use `n` arbitrarily often as an array index, without any further bounds-checking. > (2) Obtain three `foo.Index` values `a,b,c`. Test once whether the arrays `foo` and `bar` have the same length. Use `a,b,c` arbitrarily often as values of type `bar.Index`, without any further bounds-checking. I see no reason these things wouldn't be possible to implement in the language, though one would have to pass around the (phantom) evidence that these things are true to the point where it's used, which is cumbersome and something newer languages fix. I'm not saying any of this is as easy as it should be, I'm asking how "real" dependent types would be different from what Scala currently has. > Are those casts safe without runtime checks? No, we'd make the runtime check at the point of casting. What I mean is: the only way something I'd want to type as an array of length n could ever get into my program is (ultimately, once we flatten out all the arithmetic from e.g. concatenating arrays of length p and q), either a literal array of length n, or a manually checked cast of a dynamic-length array received at runtime. > In any case, at some point using types for program verification offers diminishing returns. We have to accept the possibility that maybe it's us, not type checkers, who have to verify our programs. My experience has been that types are more than good enough. My defect rate is much, much lower than it needs to be, lower than I can really justify putting any more work into, and I don't feel like I'm close to the limits of what's possible with types.
- catnaroek 9y ago
  > I can do that in Scala with monadic regions, which only need existentials/rank-2 types. Monadic regions are inflexible. As I have previously told you on lobste.rs, try implementing braided allocations: (0) Allocate A (1) Allocate B, do something with A and B together, deallocate A (2) Allocate C, do something with B and C together, deallocate B (3) etc. Turns out, you can't, because monadic regions are strictly LIFO. Lest you think this is just a theoretical exercise, this allocation pattern is used in the implementation of concurrent database indices. > I see no reason these things wouldn't be possible to implement in the language, though one would have to pass around the (phantom) evidence that these things are true to the point where it's used, which is cumbersome and something newer languages fix. The only way you could do it is if the design of the array data type anticipates every use case (including ones not in my original list). To give you an analogy, your response is exactly the same as if someone said “I don't need sum types. I can anticipate every single way in which a sum will be case-analyzed, and turn it into virtual method of a base abstract class.” This is completely ridiculous. > No, we'd make the runtime check at the point of casting. Then it's effectively dynamically typed, don't you think? > My experience has been that types are more than good enough. Types are good enough for some things. I certainly wouldn't want to program in a completely typeless language - parametric polymorphism and algebraic data types are just too nice to give up. But I also wouldn't want to use types to prove everything. Nor would you, as evidenced by your follow-up. > My defect rate is much, much lower than it needs to be Lucky you. Mine has to be zero, but it's always positive, sadly.
  - lmm 9y ago
    > Monadic regions are inflexible. As I have previously told you on lobste.rs, try implementing braided allocations: Earlier in this thread you said "this complexity only yields at best marginal increases in the extent to which these languages aid software verification. Effort would be better spent trying to figure out how much verification you can wrangle out of relatively simple type systems like ML's" - aren't monadic regions exactly a case of wrangling more verification out of a relatively simple type system rather than building something more complex? There will always be things we don't know how to do; monadic regions themselves seemed impossible until they were implemented. I don't think we've put anywhere near enough effort in yet to conclude that it's impossible to extend that kind of approach to support braided allocations; indeed that's the sort of thing I'd expect the academic process you deride to come up with. > The only way you could do it is if the design of the array data type anticipates every use case (including ones not in my original list). The Scala type system can implement Turing-complete computation, you can do arithmetic with type-level numbers, so I don't see that the array design would needs to anticipate anything? Accessing a specific element could demand evidence that that element was within the array's bounds, operations that form new arrays would need to provide evidence about that array's bounds. But the user is free to connect those two ends together in arbitrary ways. > To give you an analogy, your response is exactly the same as if someone said “I don't need sum types. I can anticipate every single way in which a sum will be case-analyzed, and turn it into virtual method of a base abstract class.” This is completely ridiculous. Um, I do say this. In a language that has first-class functions etc. I don't need any language-level support for sum types (e.g. pattern matching); Either#fold covers all the same use case. Language support is a nice syntactic convenience but nothing more than that AFAICS. > Then it's effectively dynamically typed, don't you think? No, because the type system is still checking that my deductions are valid, that my conclusions follow from my premises (e.g. if I concatenate an array that I've dynamically checked to be of size n with one that I've dynamically checked to be of size m, I statically know that the result is of size n + m). I'm just adopting an extra premise of "this particular runtime size check is correctly implemented"; of course if I adopt a false premise then I'll deduce nonsense, but that's on me. I don't see any qualitative difference between having the (outside array of unknown size -> array typed as being of a given size) function be part of the system versus implemented by me. > Types are good enough for some things. I certainly wouldn't want to program in a completely typeless language - parametric polymorphism and algebraic data types are just too nice to give up. But I also wouldn't want to use types to prove everything. Nor would you, as evidenced by your follow-up. I don't prove everything, but I feel like I could; since I'm going to be using types anyway, I don't feel the need to pursue non-type ways of proving things unless and until I hit something that I want to prove that's harder to prove with types than it should be, that feels like an easier way to prove it should exist. So far I haven't.

lmm 9y ago

> (0) The obvious: Be sure your program won't attempt to read from or write to a close file. I can do that in Scala with monadic regions, which only need existentials/rank-2 types. > (1) Obtain an arbitrary integer `n`. Test once whether it is a valid array index. If the test succeeds, use `n` arbitrarily often as an array index, without any further bounds-checking. > (2) Obtain three `foo.Index` values `a,b,c`. Test once whether the arrays `foo` and `bar` have the same length. Use `a,b,c` arbitrarily often as values of type `bar.Index`, without any further bounds-checking. I see no reason these things wouldn't be possible to implement in the language, though one would have to pass around the (phantom) evidence that these things are true to the point where it's used, which is cumbersome and something newer languages fix. I'm not saying any of this is as easy as it should be, I'm asking how "real" dependent types would be different from what Scala currently has. > Are those casts safe without runtime checks? No, we'd make the runtime check at the point of casting. What I mean is: the only way something I'd want to type as an array of length n could ever get into my program is (ultimately, once we flatten out all the arithmetic from e.g. concatenating arrays of length p and q), either a literal array of length n, or a manually checked cast of a dynamic-length array received at runtime. > In any case, at some point using types for program verification offers diminishing returns. We have to accept the possibility that maybe it's us, not type checkers, who have to verify our programs. My experience has been that types are more than good enough. My defect rate is much, much lower than it needs to be, lower than I can really justify putting any more work into, and I don't feel like I'm close to the limits of what's possible with types.

catnaroek 9y ago
> I can do that in Scala with monadic regions, which only need existentials/rank-2 types. Monadic regions are inflexible. As I have previously told you on lobste.rs, try implementing braided allocations: (0) Allocate A (1) Allocate B, do something with A and B together, deallocate A (2) Allocate C, do something with B and C together, deallocate B (3) etc. Turns out, you can't, because monadic regions are strictly LIFO. Lest you think this is just a theoretical exercise, this allocation pattern is used in the implementation of concurrent database indices. > I see no reason these things wouldn't be possible to implement in the language, though one would have to pass around the (phantom) evidence that these things are true to the point where it's used, which is cumbersome and something newer languages fix. The only way you could do it is if the design of the array data type anticipates every use case (including ones not in my original list). To give you an analogy, your response is exactly the same as if someone said “I don't need sum types. I can anticipate every single way in which a sum will be case-analyzed, and turn it into virtual method of a base abstract class.” This is completely ridiculous. > No, we'd make the runtime check at the point of casting. Then it's effectively dynamically typed, don't you think? > My experience has been that types are more than good enough. Types are good enough for some things. I certainly wouldn't want to program in a completely typeless language - parametric polymorphism and algebraic data types are just too nice to give up. But I also wouldn't want to use types to prove everything. Nor would you, as evidenced by your follow-up. > My defect rate is much, much lower than it needs to be Lucky you. Mine has to be zero, but it's always positive, sadly.
- lmm 9y ago
  > Monadic regions are inflexible. As I have previously told you on lobste.rs, try implementing braided allocations: Earlier in this thread you said "this complexity only yields at best marginal increases in the extent to which these languages aid software verification. Effort would be better spent trying to figure out how much verification you can wrangle out of relatively simple type systems like ML's" - aren't monadic regions exactly a case of wrangling more verification out of a relatively simple type system rather than building something more complex? There will always be things we don't know how to do; monadic regions themselves seemed impossible until they were implemented. I don't think we've put anywhere near enough effort in yet to conclude that it's impossible to extend that kind of approach to support braided allocations; indeed that's the sort of thing I'd expect the academic process you deride to come up with. > The only way you could do it is if the design of the array data type anticipates every use case (including ones not in my original list). The Scala type system can implement Turing-complete computation, you can do arithmetic with type-level numbers, so I don't see that the array design would needs to anticipate anything? Accessing a specific element could demand evidence that that element was within the array's bounds, operations that form new arrays would need to provide evidence about that array's bounds. But the user is free to connect those two ends together in arbitrary ways. > To give you an analogy, your response is exactly the same as if someone said “I don't need sum types. I can anticipate every single way in which a sum will be case-analyzed, and turn it into virtual method of a base abstract class.” This is completely ridiculous. Um, I do say this. In a language that has first-class functions etc. I don't need any language-level support for sum types (e.g. pattern matching); Either#fold covers all the same use case. Language support is a nice syntactic convenience but nothing more than that AFAICS. > Then it's effectively dynamically typed, don't you think? No, because the type system is still checking that my deductions are valid, that my conclusions follow from my premises (e.g. if I concatenate an array that I've dynamically checked to be of size n with one that I've dynamically checked to be of size m, I statically know that the result is of size n + m). I'm just adopting an extra premise of "this particular runtime size check is correctly implemented"; of course if I adopt a false premise then I'll deduce nonsense, but that's on me. I don't see any qualitative difference between having the (outside array of unknown size -> array typed as being of a given size) function be part of the system versus implemented by me. > Types are good enough for some things. I certainly wouldn't want to program in a completely typeless language - parametric polymorphism and algebraic data types are just too nice to give up. But I also wouldn't want to use types to prove everything. Nor would you, as evidenced by your follow-up. I don't prove everything, but I feel like I could; since I'm going to be using types anyway, I don't feel the need to pursue non-type ways of proving things unless and until I hit something that I want to prove that's harder to prove with types than it should be, that feels like an easier way to prove it should exist. So far I haven't.