On 2 Apr 2015 07:10, "Keean Schupke" <[email protected]> wrote: > > > 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.
Sorry, that should read "we don't want to introduce impredicate types". Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
