On Thu, Apr 2, 2015 at 2:01 AM, Matt Oliveri <[email protected]> wrote:
> > A 'kind' seems to me to be a PL term that is not actually part of > > intuitionistic logic / type theory, that is equivalent to 'universe 1'. > I don't think that's correct. The term "kind" is used generically to refer to a type that is rank 2 or higher. It's actually rather strongly connected to type theory. :-) The danger of higher order type systems is that many aspects of type inference become generally undecidable, so the use and propagation of kinding have to be considered with care.. > I maintain that for the sake of predicativity, there's no > need to distinguish _Bool from Bool. (That is, the Bool kind from the > bool type.) However, we want to distinguish them anyway to avoid > dependent types. > The reason this works is that literals can be viewed as behaving like types, and doing so doesn't *quite* push you over the edge into dependent types. What pushes you into dependent types is allowing *values* as arguments in type constructors. > So getting back to the original problem, do we now agree that Bool > kind is predicative? And that it makes sense for the y/n on an arrow > to be of that kind? The only reason I can see not to do this is driven by documentation concerns and possible strange unifications. Whatever it is clearly behaves like Bool kind, but we might want to do a name change for clarity. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
