On Wed, Apr 1, 2015 at 1:40 PM, Keean Schupke <[email protected]> wrote: > Going back to this, we should get: > >> def keean f a b c d tst { >> if tst >> f a b >> else >> f a b c d >> } > > keean : (a -?r1-> b -y-> c -?r2-> d -y-> j) -n-> a -n-> b -n-> c -n-> d -n-> > Bool -y-> c -?r2-> d -y-> j
We haven't actually been writing out whole types with y/n arrows. Too hard to read. :) > I see now why '?r' needs to be a kind of variable, because we want to > maintain the 'link' between arrows, so that whatever ?r2 gets bound to (n or > y) is forced to be the same as all uses of ?r2 be the same. Yeah. > The slightly worrying thing is now arrows have 'identity' in the same way a > type-variables are distinct. Why is this worrying? > 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. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
