I think we have differing ideas of what a refinement type is. My
understanding is a refinement type refines some existing type with a
restriction like:

Int < 3

Is a refinement of Int restricted to values less than three. So this is an
orthagonal concern to intersection types.

type-classes which are constraints on types give a mechanism through with
refinement types can be implemented:

(Integer a, LessThan a Three) => a

The difference is that the type classes come from the functions and get
propagated through the types automatically by inference.

Just to explain this type class:

area :: (RightTriangle a b, Numeric b) => a -> b

'a' is the type of the collection, and 'b' is the numeric base type (Int
Float etc) used in the points in the polygon. So area is a function from
polygon to a number.


Keean.


On 5 June 2015 at 20:26, Matt Oliveri <[email protected]> wrote:

> On Fri, Jun 5, 2015 at 5:46 AM, Keean Schupke <[email protected]> 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).
>
> This doesn't add up. If a's a polygon, what is (a -> b)? How do you
> take arguments that are elements of a polygon?
>
> Or did you mean for "a" to be some type that can represent right
> triangles, and not an element of a generic polygon type? That would
> make more sense.
>
> > 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.
>
> Well first of all, Matt Rice started with just Triangle, hard-coded to
> have three points. If you start with polygon, then yeah, you could
> refine down to triangles, right triangles, squares, regular septagons,
> or whatever.
>
> You have a point about wanting to be able to optimize area for
> particular polygon types. Type classes may indeed be better than
> refinements for this. I didn't mean to argue otherwise. This started
> as an example of how you _could_ use refinement types, I thought.
> (Since this is the "refinement types" thread.)
> _______________________________________________
> bitc-dev mailing list
> [email protected]
> http://www.coyotos.org/mailman/listinfo/bitc-dev
>
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to