On Thu, Apr 2, 2015 at 5:17 PM, Jonathan S. Shapiro <[email protected]> wrote: > 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. :-)
Keean and I have been counting the ranks as 0 and 1, so value types are rank 0. I figured this makes kinds rank 1. >> 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. Keean's _Bool and Bool are my Bool and bool, respectively. If we said the Bool kind was the same as the bool type, then we'd have (->) : bool -> Type -> Type -> Type I think that qualifies as dependent types. For example, we'd have to do something to prevent impure bool computations from appearing in an arrow. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
