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. _______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
