On Thu, Apr 2, 2015 at 6:26 AM, Keean Schupke <[email protected]> wrote: > On 2 April 2015 at 11:20, Keean Schupke <[email protected]> wrote: >> On 2 April 2015 at 11:01, Matt Oliveri <[email protected]> wrote: >>> Kind >>> | Bool >>> | | True >>> | | False >>> | >>> | Type >>> | | bool >>> | | | true >>> | | | false >>> | | >>> | | int >>> | | float >>> | | etc... >> >> This doesn't look like type-theory to me. > > Sorry, now I look at it more closely you have 'bool' as a type and 'Bool' as > a kind. This is exactly what I had in my original table, but its just not > intuitionistic type theory. > > Its probably fine, but the intuitionistic type-theory universes are an > alternative way of formulating this, that seems bit better to me.
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. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
