On Sun, Jul 20, 2014 at 8:06 PM, William ML Leslie < [email protected]> wrote:
> On 21/07/2014 1:00 pm, "Jonathan S. Shapiro" <[email protected]> wrote: > > OK. This is an interesting example. The example itself is clearly > contrived, but it illustrates a problem that actually does arise in > practice, which is data structure instances that meet some interesting > constraint. In this case the right-angle constraint. > > > > This can be viewed as type, or it can be viewed as a known constraint on > a value of some type. How do we want to think about this case? > > > > Incidentally, this is the kind of think that preconditions, > postconditions, and assertions deal with quite well. > > > > I think this is what Matt means by Curry types. > > There seems to be a lot of literature in that area; it seems it will take > a while before I have even a feeling for what will scale and what will be > pleasant. > So far as I know, the Curry vs. Church argument has never extended to qualified types (which didn't then exist) or constraints on values. I think the way to describe the difference is that the Church view states that types are stated with the intent to provide a prescriptive, constrained declaration of what is supposed to be true, while the Curry view seeks to derive a maximally inclusive (therefore *least* constraining) type for an existing program. I may have those backwards. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
