On Thu, Apr 2, 2015 at 7:57 AM, Keean Schupke <[email protected]> wrote: > On 2 April 2015 at 12:10, Matt Oliveri <[email protected]> wrote: >> On Thu, Apr 2, 2015 at 6:20 AM, Keean Schupke <[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?.
For example, a type constructor would be a predicate. A boolean would still be a boolean. >> 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. If you're saying 3, True, and False are types, then no. That is an accident of the Haskell encoding. They should not be types in BitC. As it happens, they aren't types in MLTT either, so I don't know why you want them to be 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? Never mind, that's not really a fair thing to say, since I'm sure some of them would be open to a language combining systems programming and constructive logic. But I'm pretty sure Shap's not interested in providing any support for constructive logic in BitC. > 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. I don't think that's necessarily true. That's one definition of "type theory"; as a shorthand for Martin-Lof type theory. But more generally, type theory is the study of type systems used as logics. > Hence ITT refers to > Impredicative Type Theory (the intuituinistic is dropped because its > implied). Actually, hardly anyone talks about Martin-Lof's impredicative type theory, since it was inconsistent. When they do, they tend to call it "Type : Type". I use ITT as an acronym for Intensional Type Theory. > Yes Type Theory is a specific mathematical theory, like category theory, and > set theory. And those are also broad areas, each with more than one particular system to study. >> >> >> 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. Universe inference is technically outside of the formal system, but basically yes. That is why there is only one type of booleans. >> 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. > >> 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. Formal logics also need to have practical proof checking. So both reasons are valid. But the thing you seem to be ignoring is that the logic that Curry-Howard corresponds to BitC's type system is inconsistent anyway, so the first reason does not apply. >> 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. In that case practical programming languages are nothing but trouble. Go home. ;) Seriously, you _did_ realize that all practical languages have features which make them inconsistent as logics, right? So what are you really getting at? _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
