On 2 Apr 2015 05:38, "Matt Oliveri" <[email protected]> wrote: > > On Wed, Apr 1, 2015 at 6:56 PM, Keean Schupke <[email protected]> wrote: > > On 1 April 2015 at 19:44, Matt Oliveri <[email protected]> wrote: > >> No, it's just a type-level boolean, conceptually. I don't know if > >> Shap's actually going to make them variables of kind Bool though. > > > > > > After thought I have realised we can consider an arrow to be a ternary > > operator (you may have already realised this). > > > > If we consider Y and N to be unit types, then we can simply have, using > > prolog notation: > > > > arrow(y, A, B) > > arrow(n, A, B) > > arrow(M, A, B) > > That is essentially what you'd do if arrows are really binary type > constructors (other than the callvar position). But like I wrote > yesterday, there's the issue of (int -n-> int), so it's not a given > that arrows are binary. > > > And this now works with standard unification. In other words 'M' is a normal > > type variable, and 'y' and 'n' simply any two distinct unit types. > > 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 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. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
