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. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
