On Mon, Jul 21, 2014 at 12:18 PM, Jonathan S. Shapiro <[email protected]> wrote: > 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.
Well Robert Constable once called Nuprl Curry-style dependent types, so it's not me who hijacked the term that time. The places I'm aware of where I might be overusing "Curry" is when "refinement" might be more appropriate. Pure Curry-style systems are essentially refinement type systems over a single Church-style type. Most typed languages have more than one Church-style type though. I still wanted to think of refinement types as possibly-impure Curry-style systems, because my concerns about completeness (Fred) don't have much to do with the underlying Church types, so I can treat both cases at once. Would you prefer if I called them refinement types? > 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. I'm not sure what you mean here, but the stuff below bothers me more. > 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. I don't see why Church vs. Curry alone would influence how hard proofs are to deal with. > 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. I don't know what you mean by curry-style inference. I'm starting to worry that by "Curry-style typing" you're thinking "no type annotations". This is rarely the case in practice, because without enough annotations, type checking can become impossible. For me the difference is that the annotations for Curry-style typing are guaranteed to be computationally irrelevant. (Because they are thought of as a type checking crutch outside the true language.) > There's > always going to be assembly code, and consequently there will be types that > are declared church-style as axioms. You mean to declare new machine-primitive types? Then I agree. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
