On Thu, Jul 10, 2014 at 8:07 PM, Matt Oliveri <[email protected]> wrote: > On Thu, Jul 10, 2014 at 6:22 PM, Geoffrey Irving <[email protected]> wrote: >> If we manage to go the extensible proof checker >> route, we can make everyone happy (or at least as happy as can be >> expected). Let's move this discussion to the thread I just started >> with the better name. > > I don't think extensible checking helps here. If I'm understanding > correctly, Shap will not want to use language features unless someone > comes up with sufficiently well-behaved type inference for it. In > principle, extensible checking would allow the inference to be added > outside the core language, but if there _is_ no way to do inference, > some features shouldn't have gone into the core language in the first > place.
When I wrote this I was thinking in particular about dependently typed pattern matching. Coq's dependent match is perfectly well behaved if all the "return" and "as" clauses are added, so my impression is that this kind of feature is something Shap might be willing to add to the language. One would then gradually relax the need for "return" and "as" with fancier and fancier extensible checkers (here we're necessarily blurring the line between checker and inferer), similar to how Coq is gradually getting smarter as versions progress. Geoffrey _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
