On 05/27/2016 01:18 PM, OndÅej KunÄar wrote:

Therefore we impose an additional restriction that makes the problem
quadratic. I call the restriction composability:
for all  d_\tau == ... and
c == ... d_\sigma ...
\sigma must be an instance of \tau or \tau must be an instance of \sigma.
(More can be found in my PhD thesis (chapter 3.5)).


Of course, I missed one case.

\sigma must be an instance of \tau or \tau must be an instance of \sigma *or they are not unifiable*.


That said, composability wants to rule out the case that the two types have a non-trivial common instance.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.