On 8 June 2015 at 20:57, Matt Oliveri <[email protected]> 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. > 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. 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. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
