On 1 April 2015 at 19:44, Matt Oliveri <[email protected]> wrote: > > > The slightly worrying thing is now arrows have 'identity' in the same > way a > > type-variables are distinct. > > Why is this worrying? >
I have thought about this and I think I have overcome my concerns. > > > I guess really -?r-> is a type variable of kind * -> *, compared with a > > normal type variable that has kind '*'. Does that make sense? > > 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) 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. If we were using Haskell like types we might write: a -Y-> b a -N-> b a -m-> b Or ML like types: 'a -y-> 'b 'a -n-> 'b 'a -'m-> 'b This is a ternary type operator in the same way that "a ? b : c" is a ternary operator in 'C'. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
