On Fri, Jun 5, 2015 at 5:55 PM, Matt Rice <[email protected]> wrote: > On Fri, Jun 5, 2015 at 2:42 PM, Matt Oliveri <[email protected]> wrote: >> On Fri, Jun 5, 2015 at 7:02 AM, Matt Rice <[email protected]> wrote: >>> I don't think we disagree here, I was (at least in my earlier emails) >>> trying to leave open the possibility that an assertion is memoized and >>> inextricably linked to the value, I probably lost this distinction >>> along the way, sorry... >> >> But with refinement types, the rightness of a triangle (for example) >> is not actually stored anywhere at runtime, and it isn't necessarily >> dynamically checked by anyone either. If I make the constant triangle >> [(0,0),(0,3),(4,0)], we can statically see that it's right, and give >> it type RightTriangle, without runtime having any trace of it being >> right. >> >> So I don't know why you're talking about memoizing assertions, as if >> refinement types were some runtime checking apparatus. > > Right the way I was thinking about it is that these could be optimized out, > e.g. > for some subprogram under which there are only right triangles, the > RightTriangle'ness would be /True/, that is it's a form of '(Type, > TypeState)'[1] pair > > such that in the absence of the ability to invalidate the typestate > (through construction of types that do not adhere to the typestate), > or mutation of the values asserted for we can say that the type > entails the typestate... > > does that attempt at an explaination help at all? > > 1: http://www.cs.cmu.edu/~aldrich/papers/classic/tse12-typestate.pdf
I'm afraid not. Refinement types make sense even in pure functional programs, so I can't figure out why you're talking about typestate. Also, with the kind of refinement type system I'm thinking of, you cannot think of a refinement as a dynamic check that's been optimized out, because the dynamic check might fail, and so the program might throw a failed assertion. A refinement cannot dynamically fail; it needs to be statically proven correct. Also, not all predicates are decidable, and you can refine with an undecidable predicate. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
