On Fri, Jun 5, 2015 at 3:39 PM, Keean Schupke <[email protected]> wrote:
> 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.
Yeah, that's my idea of a refinement type too.
> So this is an
> orthagonal concern to intersection types.
But that's not true. We can intersect (Int < 3) (Though I'd prefer to
write it {z:Int | z < 3}.) With the evens, {z:Int | z % 2 == 0}, to
get the type of evens less than 3: {z:Int | z < 3 && z % 2 == 0}. (I'm
making up the syntax for predicates.)
We can even intersect types that are refinements of incompatible
unrefined types, and get the empty type. Like the intersection of Int
and Float is empty. Maybe that's the part you don't like, where we're
not just taking conjunctions of predicates. But you can see that at
least within a given unrefined type, conjunctions give us
intersections.
> type-classes which are constraints on types give a mechanism through with
> refinement types can be implemented:
>
> (Integer a, LessThan a Three) => a
Maybe I'm being dense here, but there's a very big difference between
constraints on types and constraints on values, because types and
values are not the same. Are you using the Haskell hack of encoding
values as dummy types? If so, how do you connect these types to the
actual runtime values? (I think you might've shown me this already,
but I forgot.)
> The difference is that the type classes come from the functions and get
> propagated through the types automatically by inference.
Well hold up. Refinement types and type class resolution are not
mutually exclusive, so let's pin down the difference in meaning
between refinement types and whatever you're doing before we talk
about how to type check it.
> 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.
Let me try and understand LessThan first.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
