On Mon, Jun 8, 2015 at 4:18 PM, Keean Schupke <ke...@fry-it.com> wrote:
> On 8 June 2015 at 20:57, Matt Oliveri <atma...@gmail.com> wrote:
>>
>> 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.
>
> Sometimes we do want them available at runtime. Sometimes they have to be at
> runtime because you don't know the values until runtime.So first of all, notice that a given int belongs to _many_ ranges. So which one is it that you want around at runtime? You are still not getting it. Without refinement types, you are forced to pick a type that describes something as it is intended to be used. The more ways you intend for something to be used, the harder you have to work to find a best type. Once you have refinement types, all types that accurately describe something are assigned to it. Whether these types are useful or not. No matter how you want to use it, if it's (provably) safe, you can prove it has the appropriate type. It's a completely different way of thinking about the role of types. Of course you can still provide a way to compute a range at runtime, and use refinement types to point out that an int falls in that computable range (if in fact it does). On the other hand, with the type class you brought up, it doesn't seem possible to say an int falls in a range unless that range can be computed at runtime. >> 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. > > I get this, but you don't wan't dubl to have all those types. You want it to > have a principal type. No, Keean, _you_ don't want dubl to have all those types. I in fact do, and I don't give a rat's ass about principle types, frankly. With refinement, every object has a most specific type which is a singleton type. Boring. Principle types are only interesting in weak type systems. > As such dubl would be: > dubl :: forall a . Numeric a => a -> a > > so 'a' could be any integer, float, real, complex etc. This includes any > ranged versions of integer. No, dubl only works on ints. Take another look at the code. It necessarily works on ints within a range too, because they are ints. This is getting annoying. You are telling me again what *you want* to do, while I'm only pointing out that this is different from what I did in dubl. And I believe the range type Shap has in mind is more like mine, is completely unrelated to type classes, and does not require a way to compute the range endpoints at runtime. _______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
