On Fri, Jun 5, 2015 at 6:47 AM, Keean Schupke <ke...@fry-it.com> 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? > 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. 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. _______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
