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

Reply via email to