On 2 April 2015 at 11:01, Matt Oliveri <[email protected]> wrote: > > > 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. >
I don't understand this, and is does not seem to relate to type theory. > > > - 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. > If they are at the type-level, they are type. Type constructors are values. data T x = C x x: is a type variable C: is a value, it has the type : a -> T a T: is a parametric type, of 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. > If they are at the type-level they have to be types. There is nothing else. Just like everything at the value-level is a value. Its like saying I want to have '0' which is a value (by definition) that is not a value. > - 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. > intuitionistic type theory universes are cumulative. > > > 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... > This doesn't look like type-theory to me. >> 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. > Martin-lof type theory (1971) was impredicative, later formulations introduced universes to make it predicative. > 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. > I don't really get your point here. > > 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. Yes, you are right, I was overstating my point :-) Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
