On Mon, Jul 21, 2014 at 12:29 AM, Matt Oliveri <[email protected]> wrote:
> On Mon, Jul 21, 2014 at 12:33 AM, Jonathan S. Shapiro <[email protected]> > wrote:> 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 don't know, Matt. I guess it depends on how much term hijacking you are willing to do. Nuprl *et al* are later systems "in the style of" the curry typing approach. Should we call them curry-style systems? If it's useful, then sure. Strong church-style typing requires proofs as well. If you declare things prescriptively, you still need to "explain" to the type checker why the prescription over "here" mates up with the prescription over "there" as values flow through the program. The proof can be automated or manual. I think a better way to say your last point is that curry-style systems don't work very well (subjectively) if the proofs cannot be discharged automatically. This raises an interesting *subjective* point: curry-style inference matches very well what systems programmers will actually accept in practice, because they will stop accepting solenoidally the minute they have to manually discharge a proof. Maybe later, when they have already accepted the language and the proof is serving a purpose they care about. But even then only minimally. It'll be a huge hurdle simply to get people to believe that something like a kernel can be done in a language like BitC.[*] [*] By which I mean to the same degree that this is possible in C. There's always going to be assembly code, and consequently there will be types that are declared church-style as axioms. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
