On 2 April 2015 at 10:01, Matt Oliveri <[email protected]> wrote:
> > Which is how I was originally proposing to handle this. > > > > Universe 1 Universe 0 > > _Bool True False > > _Type Int Float Bool etc... > > OK, I see what you're saying, and this is acceptable. To be pedantic, > a universe is a type, so the left half of that table is OK; it says > _Bool and _Type are elements of Universe1. But Int, Float, Bool... are > elements of _Type; there is nothing actually called Universe0. True > and False are elements of _Bool, I assume. They are not types; _Type > is a universe, but _Bool is not. > I see my table is misleading as everything should be inside Universe 1. - Universe 0 consists of all "types" introduced so far, this includes True, False, Int, Float etc... - We assign types as labels to each type so label(True) = _Bool, label(Int) = _Type - Universe 1 is all the types in Universe 0 + the two new types we have labelled our types with. So actually: Universe 1: | | _Type | _Bool | | Universe 0 | | | | True | | False | | Int | | Float | | etc.. | | > When I wrote Bool and Type above, I meant what you are calling _Bool > and _Type. 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. > We do need to distinguish Bool from _Bool. Otherwise we get impredicativity. Thats the whole point of putting _Type and _Bool into universe 1. If we squash both universes into one, that is the very definition of impredicativity. Predicativity requires stratification. > 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? So now we can say an arrow is a ternary operator with type: (->) : _Bool -> _Type -> _Type And that works for me. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
