Closed snowleopard closed 8 years ago
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.
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).
We could treat Input a
and Output a
as completely different signals, which seems to solve the problem, but may be confusing.
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.
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.
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.
@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...
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!
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
.
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]
Fixed in #38.
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.