On Sat, Jun 6, 2015 at 2:35 AM, Keean Schupke <[email protected]> wrote: > On 5 Jun 2015 22:36, "Matt Oliveri" <[email protected]> wrote: >> >> On Fri, Jun 5, 2015 at 6:47 AM, Keean Schupke <[email protected]> wrote: >> > My point was you do not want assertions on types, abstract or not. The >> > assertions belong on the functions, as it is the algorithms that have >> > the requirements not the data. >> >> I disagree with this. What is the difference between a function that >> takes a right triangle, and a function that takes a triangle, but >> requires that it be right? There is no difference in English. There is >> no difference with refinement types. Whatever objection you have to >> associating the rightness of a triangle with its type seems to be >> based on some incorrect assumption that it's not just a different way >> of saying the same thing. >> >> In English it's very convenient to be able to say something is a right >> triangle. Why would it cause problems in a formal language? > > Alex Stepanov can explain this far more elegantly than I can, but the point > is mathematical. Algorithms have requirements, values do not.
This might be a misunderstanding due to me being sloppy about "requirement" vs. "property". I agree that values do not really have requirements. But they do have properties. (Or rather, they should be able to.) Like a triangle can be right. This does not entail that anyone actually cares that that triangle is right. But as a matter of fact, it is. > Consider the scale function, this should be able to scale any collection of > values. OK. > Then consider the area function for a square, obviously the area function > for a square is only valid on squares, but we do not want to write a square > specific scaling function. You don't need to write a square-specific scale function. You could write a function that scales arbitrary polygons (represented as a list of points). This function already _is_ a function that scales squares. We merely point this out, by giving the same polygon scaling function another type. > Putting the constraints on values results in a proliferation of redundant > code, and larger harder to read, understand and debug programs. What are you basing that on? I suspect you are basing it on an incorrect assumption about how refinement types work. Like that you'd need to write scale again just to point out that it works on squares. (Pfft!) >> > The type class "RightTriangle" can be seen as a witness to the proof >> > that the value passed to the function is a right-triangle. >> > You don't have to do this proof for every function, >> > as only right-triangles would be a member >> > of this type-class. >> >> Keean, the members of type classes are types, I believe, and triangles >> aren't types. You're on the right track, in that something just like >> type class resolution could propagate the rightness of a triangle. But >> it wouldn't actually be a type class because a triangle isn't a type. > > A type class can depend on the structure of the type not just the specific > type name, so a triangle could be a three-tuple of points. We can infer that > any three-tuple of points is a member of the triangle type class. OK, suppose it's just a Triangle type class. You're responses seem inconsistent. Are the members of Triangle types whose elements represent triangles, or are the members of Triangle themselves triangles? >> Maybe I'm finally going to find out why you were saying everything is >> a type. What you really seem to want is type class resolution, but for >> arbitrary predicates. That is fine, but making everything a type is >> definitely the wrong way to think about it. > > Type class resolution already works for arbitrary predicates on types. > Haskell has multiple argument type classes. Keean, by "arbitrary predicates" I meant "predicates on things that need not be types". I already knew type classes can be used as predicates on types, and I figured you knew it too. So the "but" before "for arbitrary predicates" should've signaled that I am talking about something else, and that arbitrary predicates on types are not "arbitrary" enough in my opinion. There seem to be two options to use type class resolution for reasoning about values. What you seem to be proposing to do is lift the values to types, and use type classes as predicates on these types which are the lifted values. I'm proposing instead to generalize type classes to be "arbitrary predicates", so we don't _have_ to lift the values. (Maybe this is what you were getting at with "value classes".) What I was asking is whether your way of using type classes to reason about values was the reason for you to think of everything as a type. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
