On Thu, Jul 10, 2014 at 11:12 PM, Geoffrey Irving <[email protected]> wrote: > 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.
OK. That's a good example of how an extension could've added inference. We'll just have to see what Shap thinks. In principle lots of design decisions could be pushed to checker extensions, but not without a huge change to the design philosophy of the core language. A big difference between BitC and what I want to do with extensible checking is that I already want the user-facing language to be basically built up with extensions, and don't care much what the base language looks like. But I'd be surprised (in a good way!) if Shap would want to try that. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
