On Thu, Apr 2, 2015 at 6:20 AM, Keean Schupke <[email protected]> wrote: > On 2 April 2015 at 11:01, Matt Oliveri <[email protected]> wrote: >> On Thu, Apr 2, 2015 at 5:31 AM, Keean Schupke <[email protected]> wrote: >> > - 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.
A type should be able to appear to the right of the typing colon. You cannot put just a type constructor to the right of a colon; you need to apply it first. Type constructors are not types. And neither are True or False, as in the y and n for an arrow. I know you proposed that y and n would be unit types, but I am telling you there's no need for that. > Type constructors are values. I would prefer to reserve "value" for elements that are not type-level. > 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 * -> * This all seems right. Note that parametric types are not literally types in the right-of-the-colon sense. They are families of types. Parameterized types are types in the same sense that parameterized modules (ML functors) are modules: They aren't, until you apply them. >> > - 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. This is just plain false. I don't know how you got this idea, and it's leading you to an overcomplicated design. Maybe it's Haskell's fault. Haskellers have a penchant for abusing types for things that are morally type-level data, because Haskell presumably doesn't have enough kinds. > Just like everything at the value-level is a value. Everything at the value level (elements of types of the lowest universe) is a non-type because the situation degenerates. There cannot be value-level types, because it would mean the universe of values wasn't the lowest after all. In other words, the universe of values contains only types which are not themselves universes. This situation does not generalize. If that's not what you're talking about, then I can't follow your argument. >> > - 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. That's true. BitC is emphatically not intuitionistic type theory. Type theorists and systems programmers alike would be very miserable if it were. >> > 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. It's a textbook case of type theory. I must assume that you haven't learned type universes correctly. At least not in full generality. Even if this kind of type system is something I made up all by myself without realizing, what disqualifies it from being type theory? >> >> 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. That is an invalid counter argument. Me: MLTT has one type of booleans. You: No, MLTT has multiple universes. See the mismatch? I am telling you that the predicative versions of MLTT (the original wasn't even consistent) have multiple universes which all share the same two-element type. Hmm. Actually, it depends on whether your universes are Russel-style or Tarski-style. I mean it really doesn't, since I defined "type" to be something the goes to the right of a colon, but with Tarski universes, each universe has a distinct element corresponding to the type of booleans. But in that scenario, you need to lift a universe element to a type to use it to the right of the colon, and there's still only one type of booleans. Lifting any universe's element for the booleans gets you the same type. Is this our misunderstanding? >> > 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. I denied what you said by contradicting it. :) There are two quite different reasons to use universes: - To control the strength and consistency of a logic - To control the expressiveness (and type checking/inference difficulty) of a type system The reason for BitC to have two types of booleans, in different universes, is only the second kind of reason. There is nothing especially strong logically about having a single type of booleans for all universes. >> > 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 :-) _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
