On Sun, Jun 7, 2015 at 2:06 AM, Keean Schupke <[email protected]> wrote: > On 6 Jun 2015 21:44, "Matt Oliveri" <[email protected]> wrote: >> On Sat, Jun 6, 2015 at 11:04 AM, Keean Schupke <[email protected]> wrote: >> > class RightTriangle container unit where ... >> > >> > So RightTriangle is a predicate that is true if the type is a right >> > triangle. >> >> So how would you code that? See this is the part I don't know how to >> do with Haskell type classes. > > Actually the mechanics of this require a lot of tedious boiler plate in > Haskell. But we can do it with polymorphic recursion.
Well see the problem is that I actually need to see something to know what we're talking about. Right triangles are not trivial enough maybe. How about even natural numbers? Or maybe you could point me to something similar. >> > So the point is functions like scale: >> > >> > scale :: Polygon a unit => unit -> a -> a >> > >> > a is a type constrained by the type-classes, that's all we ever need to >> > know >> > about it. >> >> OK. Now how would you state that scale preserves rightness of triangles? > > This makes me want to use a type for RightTriangle, but then how would I > write 'shere' where a RightTriangle may not be afterward, or a non right > triangle may become a right one? Shearing? Well I think that'd also be (Polygon c s => s->c->c). So we don't say anything about rightness at all. > How would you write a single scale function for all polygons that preserves > a rightness property? We write a scale function for all polygons. That's it. It's a mathematical fact that a correct scale function would preserve the rightness of triangles. So we can then prove that our scale function preserves rightness of triangles. Actually we need to prove it preserves triangle-ness too, since the function works with arbitrary polygons, so the unrefined type doesn't tell us that scale preserves the number of sides anymore. These proofs let us give scale another type: Polygon c s => s->RightTriangle->RightTriangle That looks weird, but RightTriangle is implicitly taking the type class instance in order to define a refined version of c. You might want different syntax for type classes if you were going to have predicates and/or refinement types. See, the idea of refinement types is that conceptually you define some value at an unrefined type, and then you ascribe more types to it which are refinements of the unrefined type. Since you already have the code written when you're assigning refinement types, the refinement types need not impact the structure of the code at all. Now that's not necessarily how it actually works, but it's a good way to think about it, I think. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
