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 think you're mixing this up with a totally different style of system. (Like classical logic.) Another way to see it is that y and n are the only "types" in some other, incompatible universe-0, and Bool _is_ that universe-0. Here again, we're predicative because Bool is not a domain of quantification. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
