On 8 Jun 2015 04:23, "Matt Oliveri" <[email protected]> wrote: > > On Sun, Jun 7, 2015 at 9:17 AM, Keean Schupke <[email protected]> wrote:
> The difference cannot be that small, unless I'm misunderstanding you > very badly. Let me try again. With refinement types, you assign types > to values/functions that accurately describe them. A value/function > can have arbitrarily many types. > > Suppose I write the function > > dubl (z:int) = 2 * z > > One of dubl's types is (range[1,4]->range[2,8]). The idea that we want > to even consider ranges is not present in the code, so your idea of > putting "begin" and "end" members in a type class already seems very > different from refinement types. Well if the refinement is a constraint on a type which is a type class, then the begin and end methods would be available to query the range. In fact querying the range creates the requirement, so for e example: f x a = if (end x) < (end a) then ... Would create a requirement something like: f :: (Range a, Range b) => a -> b -> ... Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
