-
Notifications
You must be signed in to change notification settings - Fork 0
protocolNotes
I have the state monad laws encoded and prove 2 of them. Unfortunately, it caused to other proofs to fail. I have no idea why this is. Here's the summary:
Added the 4 state monad laws:
<<< put s >> put s' = put s' put s >> get = put s >> return s get >>= put = return () get >>= λs → get >>= k s = get >>= λs → k s s
Why did the last two proof involving put and get suddenly fail? The only thing I can figure right now is that something about these generalized variables is causing it. Actually, I'm not even sure why the proofs won't go through. Need to bang on that more as well.
Diving into the definition of operations in the protocol monad. Interesting that the only parameters to the monad as of now are A and S.
What if we treat A is the message type? Does that do anything for us?
Specified the signatures of our basic protocol operations. Need to talk these through with the team before moving forward, but the A result type as the communicated type is looking pretty interesting. Still need to work through many of the type signatures.
Should the protocol be a state monad or a reader monad? That is still pending. Also, where to put the error handling mechanism.
Created the first protocol monad. Still things that bug me about it, in particular the way it is constructed initially from the StateMonad and ProtocolMonad typeclass. I would like to understand that way better than I do. More time for that later.
There seems to be a problem with typing in the class definition for StateMonad. It seems like the term doesn't know what structure to build. The type is existential, but I tried to change to be explicit earlier.
Let's try changing the return type of put and get to explicitly reference State.
Got it! By making sure that put and get know they are dealing with State types, the problem seems to be solved. I need to play around a bit more before I clean things up. Also need to find a way to annotate types without using the magic functions I need to use now. Type annotation in coq.
Pulled the type annotations out and it still works. Go figure. Something in the development modules was causing trouble.
3:43 PM - Cleaned up the definition and committed the result. Cool beans. Time to move on to the ProtocolMonad itself.
Adding some documentation and cleaning up the theory. Will use one definition of Monad.
Move the Monad typeclass into a separate file. Still need to find a references for the page where its from.