On Mon, Jul 21, 2014 at 12:33 AM, Jonathan S. Shapiro <[email protected]> wrote: > On Sun, Jul 20, 2014 at 8:06 PM, William ML Leslie > <[email protected]> wrote: >> 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.
Is that still the case if you use Curry-style typing and refinement typing interchangeably? Nuprl is a full dependent type system where all types are Curry-style. This seems to indicate that qualified types (if I know what you mean) and constraints on values should be handled fine. The problem with strong Curry-style typing seems to be the need for proofs. > 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. No, that's the right order. I think. Here's how I'd say it, since I'm not sure it means the same thing as what you said: Church typing provides a prescriptive system for deriving elements of existing types, while Curry typing provides a descriptive system to assign types to existing objects based on their semantic properties. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
