On Tue, Jul 22, 2014 at 1:36 AM, Jonathan S. Shapiro <[email protected]> wrote: > On Mon, Jul 21, 2014 at 2:20 PM, Matt Oliveri <[email protected]> wrote: >> On Mon, Jul 21, 2014 at 12:18 PM, Jonathan S. Shapiro <[email protected]> >> wrote: >> > 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. > > In curry-style typing, you need to be able to derive types from > annotation-free programs. If the resulting discharge obligations become > visible to the programmer as manual proof obligations, you're doomed.
Well, you said strong Church-style type systems can have proof obligations too. When that's true, I figured you'd say "you're doomed" there too. The annotation-free programs are what you give operational semantics, but there's nothing wrong with adding annotations as a way to handle simple proof obligations. They just get erased. That is, a Curry-style system can look awfully similar to a Church-style system, from the user's point of view. I'll admit though that interesting uses of refinement types can easily involve proof obligations that aren't syntax-directed enough to dress up as ordinary annotations. But to me, this is just paying for the ability to express stronger types. Trying to do the same things with Church-style types would be even worse. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
