On 2 April 2015 at 12:57, Keean Schupke <[email protected]> wrote: > > > 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. >
To compare with Lamba-calculus, every term in lambda calculus is a lambda, there is nothing else. However, you can represent booleans and integers with lambda expressions using Church encodings. We can take a short-cut and use familiar symbols to represent those lambda expressions: id = \a . a true = \a . \b . a false = \a . \b . b so now we can write: id true However 'true' is a lambda expression and this is important, because the laws of lambda calculus (beta reduction etc) are only expressed in terms of lambdas. Introducing something from outside of lambda calculus (another operator other than lambda) requires new axioms to be added to the system, and essentially is not lambda calculus any more and may not share any of the properties we want from lambda calculus (reduction has a normal form etc). All these things would need to be re-proved. The same is true of type theory, the axioms are defined solely types. So if you introduce something that is not a type, you need to introduce new axioms to what is now "type+whatever" theory, and re-prove all the important results. So by keeping everything a type, we avoid inventing a new system, and we keep all the existing proofs. All wee have to do is represent what we want using types (so the type-level encodings of Peano numbers are the equivalent of church encodings). Fortunately the type level encoding of a Boolean is simple, we need two types "True" and "False". Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
