On 2 April 2015 at 12:10, Matt Oliveri <[email protected]> wrote: > > > 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. >
So applying curry-howard, what does a non-type translate to in intuitionistic logic?. > 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. > Maybe, I had already decided to have an Int kind, for representing type level Ints, but this is justified because they are just a representation of Peano numbers. IE we have types Zero, and Succ x, we can construct the number three as Succ (Succ (Succ Zero)) which we can represent by the symbol "3". Note it is justified because it can be implemented in types, and although its kind is Int, it is still a type. Likewise we may declare symbols to represent "True" and "False", but they notionally map to 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. > > > > 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. > I am not sure why? > > 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. > I misread it. However the only Type Theory is intuitionistic type theory. What PL people call type systems are not actually type theory. Type Theory specifically refers to intuitionistic type theory. Hence ITT refers to Impredicative Type Theory (the intuituinistic is dropped because its implied). Even if this kind of type system is something I made up all by myself > without realizing, what disqualifies it from being type theory? > Yes Type Theory is a specific mathematical theory, like category theory, and set 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. > MLTT is a dependent types, and the Bool it lifted to the appropriate level by universe inference. > 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. > I think the lifted universe types are distinct, otherwise all the universes collapse into one. > 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? > Maybe. > I denied what you said by contradicting it. :) > This isn't an argument, its just contradiction (obligatory Monty Python quote).. > 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 > I would say the first argument is the only valid one, as a type system is logic via curry-howard. 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. > Ad-hoc type systems that do not correspond to a sound logic lead to trouble in my opinion. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
