Input, output and internal events and signals

[snowleopard]

Right now we don't distinguish between input/output/internal events and signals. I think this is one of the reasons we can't quite figure out the right way to deal with initialisation concepts #11.

Also, STGs do require to assign signals into groups so we will have to do it anyway at some point. Let's use this issue to discuss this.

[snowleopard]

A temporary solution is in the signal-types branch, in particular, see src/Tuura/Concept/Signal.hs.

However, it is not satisfactory at the moment, as one can mix Input a and Output a in one specification and it will be allowed. We probably don't want to permit this, which seems to lead to a complete separation of input/internal/output types.

Does it make sense to consider concepts parameterised by i o t instead of simply a? This looks overly verbose, inconvenient and inextensible, but is simpler (does not require GADTs or existential types) and solves the problem of mixing signals with the same name but different types in a single specification.

[snowleopard]

Note, STGs are usually defined on a set of signals S that is partitioned into non-overlapping sets I, O, and T corresponding to input, output and internal signals, respectively. We need to encode this partition nicely, preferably at the type level, and make sure we don't allow creating signals of different types but with the same name (my previous solution fails in this aspect).

[snowleopard]

We could treat Input a and Output a as completely different signals, which seems to solve the problem, but may be confusing.

[jrbeaumont]

It seems we are stuck between a rock and a hard place.

Input a and Output a could be confusing, but it's a much nicer way of viewing it. It'd be better this way I feel however.

Could we not add some verification for non-overlap of signals? It would mean the nice implementation can be used, and avoid some problems.

[snowleopard]

There is one reason we might want both Input a and Output a to be allowed. Imagine specifying behaviour of two circuits connected with a common wire:

data Signal = A | B | C

-- For circuit1 signal B is an output
circuit1 = rise (Input A) ~> rise (Output B) <> ...

-- For circuit2 signal B is an input
circuit2 = rise (Input B) ~> rise (Output C) <> ...

-- In the overall system, we compose the circuits and B is either internal or output
system = circuit1 <> circuit2 <> ...

So, we have the following possible interplay of signal types above:

• circuit1 has input A and output B
• circuit2 has input B and output C
• system has input A, output C and, perhaps, an internal signal B (if it is not used anywhere else)

Is this useful? If yes, we might want to allow both Input a and Output a.

Note that the specifications for circuit1 and circuit2 may be coming from different files, both importing the common set of interface signals {A, B, C}. Forcing B to be of certain fixed type (input, output or internal) at the definition site therefore may be too restrictive. Furthermore, assuming that circuit1 and circuit2 have no idea about the existence of each other, there is no reason why they should use Internal B instead of more natural Output B and Input B, respectively.

[jrbeaumont]

In this case could we not verify that signals are not defined as both inputs and outputs local to a scenario. I feel this is the same issue, possibly made more complicated. I didn't think of it like this, and really it would be useful for this sort of purpose, and probably a good idea to keep it therefore.

This then raises several other points, such as, do we aim to try and change signal types?
For example, if in your above example, the signal B is only used as an output from circuit1 and an input to circuit2. In this case, when composing both circuits, it would make sense for it to be an internal signal.

My question is, could/should we force it to be internal in the composition, system?
Or, could we take some sort of approach of:
Signal B is defined as both an input and an output (in two separate scenarios). Regardless of whether it is used again, it is an output of some part of the system and thus we should refer to it simply as an output from herein.

[snowleopard]

@jrbeaumont Perhaps, this leads us to a new type of concept: interfaceConcept? It could be responsible for keeping track of all signal types to make sure <> composes things correctly.

Let's assume we compose two concepts left <> right, then I think the following rules apply:

left	right	left <> right
input	input	input
input	output	output
output	output	error
unused	input	input
unused	output	output
unused	unused	unused
input	internal	error
output	internal	error
internal	internal	error?
unused	internal	internal

I think the above captures all possible combinations (up to commutativity).

Note, with the above rule, system will have Output B, not Internal B. In general I think it is the designer who should explicitly make a signal internal, thereby forbidding it to be used in further compositions.

Also, the errors above would probably be quite hard to make checkable at compile time...

[snowleopard]

Actually, errors are strange. We do want to sometimes compose two concepts with the same output! This happens in buffer, for example:

rise (Input A) ~> rise (Output B) <> fall (Input A) ~> fall (Output B)

Maybe there are no errors after all!

[snowleopard]

If we allow all possible compositions then the following seems reasonable:

left	right	left <> right	Comment
input	input	input	Same input used by two concepts
input	internal	internal	The right concept drives the signal
input	output	output	The right concept drives the signal
internal	internal	internal	Same internal signals are synchronised
internal	output	output	Synchronise an internal signal with an output
output	output	output	Same outputs are synchronised
unused	input	input	Unused signals do not interact with used ones
unused	internal	internal	Unused signals do not interact with used ones
unused	output	output	Unused signals do not interact with used ones
unused	unused	unused	Unused signals do not interact with used ones

I think the rule is actually pretty simple and is a max operator in disguise:

data SignalType = Unused | Input | Internal | Output deriving Ord

compose :: SignalType -> SignalType -> SignalType
compose = max

This means that we could implement the interfaceConcept as a sorted list of signals with types, and the composition would be something like a zipWith max.

[snowleopard]

A bit more elaborated:

data SignalType = Unused | Input | Internal | Output deriving Ord

mempty' :: Signal -> SignalType
mempty' = const Unused

mappend' :: (Signal -> SignalType) -> (Signal -> SignalType) -> Signal -> SignalType
mappend' f g = \s -> f s `max` g s

inputs :: [Signal] -> (Signal -> SignalType)
inputs ins = \s -> if s `elem` ins then Input else Unused

outputs :: [Signal] -> (Signal -> SignalType)
outputs outs = \s -> if s `elem` outs then Output else Unused

m1 :: Signal -> SignalType
m1 = inputs [a, b]

m2 :: Signal -> SignalType
m2 = outputs [b, c]

[snowleopard]

Fixed in #38.