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. A type-system has type and variables which range over the types. This maps directly into intuitionistic logic. 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? What would such a thing mean outside of an arrow? What would: not-type1 -> not_type2 mean? Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
