On Thu, Apr 2, 2015 at 4:02 AM, Keean Schupke <[email protected]> wrote: > On 2 April 2015 at 08:56, Matt Oliveri <[email protected]> wrote: >> On Thu, Apr 2, 2015 at 3:49 AM, Matt Oliveri <[email protected]> wrote: >> > On Thu, Apr 2, 2015 at 2:10 AM, Keean Schupke <[email protected]> wrote: >> >> On 2 Apr 2015 05:38, "Matt Oliveri" <[email protected]> wrote: >> >>> M should not be a type variable. What is "int -int-> int"? What's >> >>> wrong with a Bool variable? I know Prolog doesn't have types in that >> >>> sense. But on paper, or in a typed metalanguage, one should pick the >> >>> more appropriate kind. >> >> >> >> Right, but we only create arrows with y and n so that would never >> >> happen. >> >> >> >> It can't really be a simple Bool, as we [don't] want to introduce >> >> impredicate types. >> >> 'm should be a universe-1 variable ranged over y and n in universe-0 to >> >> preserve predicativaty. >> >> >> >> Personally I think its better to leave as a simple type var, or >> >> introduce >> >> higher universes. >> > >> > Impredicative? Nonsense. There are no quantifiers for it, and even if >> > there were, we could just interpret them computationally. >> >> I mean no explicit quantifiers over Bool to use freely in types. Of >> course there are the implicit quantifiers outside the types. Those are >> no worse than the implicit type quantifiers giving you ranked >> polymorphism, of course. >> >> And again, even if we did have explicit Bool quantification, this >> isn't classical logic; Bools aren't propositions. It would just be >> dependent types. > > Well we should start from intuitionistic logic for a type system, not > classical logic.
Exactly. I thought you were thinking of Bool as the type of classical truth values, because otherwise I have no clue why you'd think a Bool kind is impredicative. I assume that's what you meant by "impredicate types". > A type-system has type and variables which range over the types. This maps > directly into intuitionistic logic. Intuitionistic propositional logic, yes. Except BitC types include a lot of stuff that wouldn't make sense in IPL. Like recursive types, which would be inconsistent. > If we create a second class of thing which is a not-type that can be true or > false, and a second class of variable which ranges over not-types? That's not a complete question. > What would such a thing mean outside of an arrow? > > What would: > > not-type1 -> not_type2 > > mean? Beats me. Good thing we're not going to let anyone write that. _You_ are the one saying we should be conflating y/n with types. We're saying y/n only go on an arrow. That's it. In other words, the ternary "arrow" constructor from your earlier email should have the kind: arrow :: Bool->Type->Type->Type _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
