On Sun, Jun 7, 2015 at 9:17 AM, Keean Schupke <ke...@fry-it.com> wrote: > On 7 Jun 2015 12:04, "Matt Oliveri" <atma...@gmail.com> wrote: >> On Sun, Jun 7, 2015 at 4:26 AM, Keean Schupke <ke...@fry-it.com> wrote: >> > I general I think everything should have an interface defined by a type >> > class, so a range is any type that implements 'begin' and 'end' that >> > return >> > the beginning and end of the range. As such range is a type constraint, >> > that >> > can be inferred from a function type: >> > >> > f :: Range r => r -> r >> > >> > r can be any type, and the constraint propagates as required. >> >> This doesn't do anything like what I think Shap is talking about. For >> example, to a function that doubles an integer, you should be able to >> give the type: >> range[1,5)->range[2,10) >> Saying that if you give it an int (1 <= z < 5), you'll get an int (2 >> <= z' < 10). Come to think of it, because ints are discrete, it could >> be >> range[1,5)->range[2,9) >> in other words >> range[1,4]->range[2,8] > > I think really the difference in what we are saying is inference. If all the > algorithms specify their requirements then the constraints on the types can > all be inferred. I don't think you should manually be defining them on > types, I think you should let them be inferred (they are still there). At > the other end you have to prove the inferred requirements are met when the > type is constructed.
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. _______________________________________________ bitc-dev mailing list bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
