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. Consider the scale function, this should be able to scale any collection of values. 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. Putting the constraints on values results in a proliferation of redundant code, and larger harder to read, understand and debug programs. > > > 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. > 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.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
