On Thu, Apr 2, 2015 at 5:31 AM, Keean Schupke <[email protected]> wrote: > On 2 April 2015 at 10:01, Matt Oliveri <[email protected]> wrote: >> On Thu, Apr 2, 2015 at 4:26 AM, Keean Schupke <[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.
That is not what I'm correcting. I was not confused about that. You were saying Universe0 is inside Universe1. I'm saying Universe0 isn't really a thing. _Type is what you want to use instead. > - Universe 0 consists of all "types" introduced so far, this includes True, > False, Int, Float etc... No, True and False should not be types. They are elements of a kind, so they're type-level. This does not mean they're types. Consider type constructors. They are also type-level, but are not types. They are elements of a function kind. True and False are elements of Bool kind. > - We assign types as labels to each type so label(True) = _Bool, label(Int) > = _Type This is silly. You need to do this only because you have mistakenly grouped True and False in with the types. > - Universe 1 is all the types in Universe 0 + the two new types we have > labelled our types with. This would be sensible, but there's no need to include all types as kinds. Actually with BitC types allowing side-effects, it really would not be so sensible. > So actually: > > Universe 1: > | > | _Type > | _Bool > | > | Universe 0 > | | > | | True > | | False > | | Int > | | Float > | | etc.. > | | No: Kind | Bool | | True | | False | | Type | | bool | | | 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. You are wrong. Martin-Lof type theory is predicative and allows much more than using one bool everywhere. > Thats the whole point of putting _Type and _Bool into > universe 1. No, the point of putting them in a higher universe is because we want to use their elements as subexpressions of types without using dependent types. > If we squash both universes into one, that is the very > definition of impredicativity. Predicativity requires stratification. It is not the _definition_ of impredicativity, but it would be impredicative. However, this is because it would result in Type : Type, not because it would combine Bool and bool. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
