On Thu, Apr 2, 2015 at 4:15 AM, Matt Oliveri <[email protected]> wrote:
> We don't want intuitionistic type-theory's way, which is to use > dependent types. Dependent types for an imperative language is cutting > edge stuff, and Shap decided not to try to do that yet. shap is still very unhappy about that outcome. I would say rather that shap has decided to defer consideration of dependent types, except to make sure that we don't do something stupid in our surface syntax to preclude them. However: shap still harbors an unhappy suspicion that we *need* dependent types. Given this, I definitely think we should consider the implications of our designs in the context of the appropriate dependent type theories. Or at least that's what shap thought when I spoke to him last... shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
