-
Notifications
You must be signed in to change notification settings - Fork 7
Anti-pipelining (TODO better name) (AKA receiving despite having agency) #92
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from 11 commits
08f53ad
0ae7f49
4bfa2d3
fe2e3e2
8b39f07
41e240e
0185f7a
e54b64d
aab71cc
a0a8f17
a789d35
5b59ef8
4df5d15
c74d1f5
15e33e2
fb92601
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -44,6 +44,7 @@ module Network.TypedProtocol.Core | |
| , IsPipelined (..) | ||
| -- *** Outstanding | ||
| , Outstanding | ||
| , AntiOutstanding | ||
| -- *** N and Nat | ||
| , N (..) | ||
| , Nat (Succ, Zero) | ||
|
|
@@ -491,13 +492,17 @@ data N = Z | S N | |
| -- | Promoted data type which indicates if 'Peer' is used in | ||
| -- pipelined mode or not. | ||
| -- | ||
| data IsPipelined where | ||
| data IsPipelined ps where | ||
| -- | Pipelined peer which is using `c :: Type` for collecting responses | ||
| -- from a pipelined messages. 'N' indicates depth of pipelining. | ||
| Pipelined :: N -> Type -> IsPipelined | ||
| Pipelined :: N -> Type -> IsPipelined ps | ||
|
|
||
| -- | Non-pipelined peer. | ||
| NonPipelined :: IsPipelined | ||
| NonPipelined :: IsPipelined ps | ||
|
|
||
| -- | Pipelined peer for a /server/ that only ever uses one | ||
| -- 'Network.TypedProtocol.Peer.Sender' | ||
| AntiPipelined :: ps -> ps -> N -> IsPipelined ps | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I'm opening a threaded conversation here for this discussion of naming #92 (comment)
So, my intuition: If we don't want to rename
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. We discussed this in the call. Long-term goal:
At that point, the symmetries are clear and it's also clear that they're both pipelining something, either awaits or yields. (A single peer could conceptually do both, just not at the same time, but we don't see a need for that yet.) |
||
|
|
||
| -- | Type level count of the number of outstanding pipelined yields for which | ||
| -- we have not yet collected a receiver result. Used to | ||
|
|
@@ -506,10 +511,17 @@ data IsPipelined where | |
| -- and to ensure that the non-pipelined primitives 'Yield', 'Await' and 'Done' | ||
| -- are only used when there are none unsatisfied pipelined requests. | ||
| -- | ||
| type Outstanding :: IsPipelined -> N | ||
| type Outstanding :: IsPipelined ps -> N | ||
| type family Outstanding pl where | ||
| Outstanding 'NonPipelined = Z | ||
| Outstanding ('Pipelined n _) = n | ||
| Outstanding 'NonPipelined = Z | ||
| Outstanding ('Pipelined n _) = n | ||
| Outstanding ('AntiPipelined _ _ _) = Z | ||
|
|
||
| type AntiOutstanding :: IsPipelined ps -> N | ||
| type family AntiOutstanding pl where | ||
| AntiOutstanding 'NonPipelined = Z | ||
| AntiOutstanding ('Pipelined _ _) = Z | ||
| AntiOutstanding ('AntiPipelined _ _ n) = n | ||
|
|
||
| -- | A value level inductive natural number, indexed by the corresponding type | ||
| -- level natural number 'N'. | ||
|
|
||
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You posted a top-level question here about "proofs". #92 (review)
AntiPipelinedinto them at some point, but it never did.Pipelinedproof).There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, in our most loved theorem prover - Haskell 😉. If we implement
forgetAntiPielinedthen we can have aconnectAntiPipelinedsimilar toconnectPipeliendThere was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That's because you extended the type and guarded it at the type level with
AniPipelinedconstructor.Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
🤔 if our proofs where polymorphic in
IsPipelinedargument, then it would force you for write a proof, butconnectrequiresNonPipelinedpeers, andconnectPipelinedrequiresPipelinedones.