On Thu, Apr 2, 2015 at 5:22 PM, Jonathan S. Shapiro <[email protected]> wrote: > 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.
OK. Thanks for the correction. > 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... You talk like this it seems whenever I tell someone about what "Shap" said. I'm talking about you, of course. Your signature just says "shap". Would you like me to refer to you some other way? Or should I never try to report what you've said? _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
