> Ordered types can be used to describe elements of a (possibly bi-directional) pipeline running asynchronously. (If its synchronous I think all you need is subsignleton types.) See notes for lectures 5-10 (sep 13-sep 29) of http://www.cs.cmu.edu/~fp/courses/15816-f16/schedule.html

I am confused, what does this have to do with residuated lattices over non-commutative monoids?