[CZT-Devel] schema composition type rule - query

[Leo F. <leo...@ne...>]

Hi guys,

I think there was discussion about this, but I don't know the details. From the Standard (13.2.6.22), I infer that
the type for (LHS \semi RHS) is given by intricate filtering of bindings as follows:

a) match = all the bindings of RHS that are NextStroke decorated in LHS (e.g., match set)
b) B3       = LHS bindings  MINUS bindings of match decorated with NextStroke
c) B4 	 = RHS bindings MINUS match
d) result = B3 cup B4

ex:

S == [ x: \nat ]
T == [ y: \nat ]
LHS == [ \Delta S; in? : \nat ]
RHS == [ \Delta S; out!: \nat ]
Op == LHS \semi RHS

what are the bindings of Op? I would expect them to be x, x', in?, out! but int I/O gets filtered out by the Std def?
What if the composition is not homogenous like in 

LHS == [ \Delta S; \Delta T; in? : \nat ]
RHS == [ \Delta S; out!: \nat ]
Op == LHS \semi RHS

or 

LHS == [ \Delta S;  in? : \nat ]
RHS == [ \Delta S; \Delta T; out!: \nat ]
Op == LHS \semi RHS

bindings of Op given by the typechecker are x, x', y, y', in?, out!.... That is despite the fact there might be more dashed
variables in one side than the other. Any thoughts?

Similarly, how to trust the definition for piping?

Best,
Leo