On Mon, Jun 8, 2015 at 2:23 PM, Keean Schupke <ke...@fry-it.com> wrote:
> On 8 Jun 2015 04:23, "Matt Oliveri" <atma...@gmail.com> 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.
But that's not what I'm doing. I'm just refining int.
range[lo,hi] = {z:int | lo <= z <= hi}
We don't want the upper and lower bounds to be available at runtime,
because we often don't want to store them.
And I think you're still missing the significance of having
arbitrarily many types. dubl has all of the following types:
int->int
range[0,0]->range[0,0]
range[1,1]->range[2,2]
...
range[0,2]->range[0,4]
range[0,4]->range[0,8]
...
isect lo hi,range[lo,hi]->range[2 * lo,2 * hi] // insert disclaimer
about overflow
Clearly we cannot store all this. Refinement describes things as they
already are without affecting them.
_______________________________________________
bitc-dev mailing list
bitc-dev@coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev
