On Fri, Jun 5, 2015 at 2:42 PM, Matt Oliveri <atma...@gmail.com> wrote: > On Fri, Jun 5, 2015 at 7:02 AM, Matt Rice <ratm...@gmail.com> wrote: >> On Fri, Jun 5, 2015 at 3:47 AM, Keean Schupke <ke...@fry-it.com> wrote: >>> >>> >>> On 5 June 2015 at 11:36, Matt Rice <ratm...@gmail.com> wrote: >>>> >>>> On Fri, Jun 5, 2015 at 2:46 AM, Keean Schupke <ke...@fry-it.com> wrote: >>>> > I don't understand, you just use type-classes: >>>> > >>>> > area :: (RightTriangle a b, Numeric b) => a -> b >>>> > >>>> > RightTrianlge is a constraint on the polygon "a" with points of type "b" >>>> > (Int or Float etc). >>>> > >>>> > Only the algorithm used in areaOfRightTriangle knows the type of >>>> > triangle >>>> > required for the area operation, not the triangle itself. >>>> > >>>> > I can have other triangle area definitions too: >>>> > >>>> > area :: (Square a b, Numeric b) => a -> b >>>> > >>>> > WIth suitable overloads I can call 'area' on any polygon, and I will get >>>> > the >>>> > most efficient algorithm for that type of polygon automatically. >>>> > >>>> >>>> I guess I don't understand how this in any way affects what I was >>>> replying to, which was coalescing assertions on types that were not >>>> abstract... >>>> >>>> but in reality probably just more comfortable/familiar with the keykos >>>> model of lambda calculus which doesn't assume you'd ever want to give >>>> out a constructor... >>> >>> >>> My point was you do not want assertions on types, abstract or not. >> >> 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 _______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
