We move the effort into designing the type, so that writing the algorithm is simpler.
There is a relationship between monads and Hoare Logic. Can I solve the 9-jigsaw puzzle with Monads? https://en.wikipedia.org/wiki/Hoare_logic
Types capture our requirements.
His coding demos were totally type-hole driven.
Exception occur when the run-time does not know what to do. Errors occur when the programmer doesn’t know what to do..
- Joe Armstrong
[In the Erlang way of thinking] errors are the lack of specification.
“Eventual consistency” is a vague term. Instead:
- Eventual Delivery: Eventually, every operation seen by every node. (Asynchronous - may be received in any order.)
- Convergence: Seen same operations == Has same state. (Again, regardless of order.)
- Don’t lose data: otherwise it’s easy! ;-)
Each node has an ID.
Each term has an ID.
When adding a new term, give it the ID (largest ID seen so far + 1 :: Node_Name).
| h | 1a |
| e | 2a |
| l | 3a |
| o | 4a |
Send a message like, “Insert ‘l’ with ID 4b after item 2a.”
When you delete, you don’t delete data - you might get an operation that saying “insert after 2a”, but 2a has gone. Instead, you “tombstone” 2a and if such a message comes along, you just step forward to the first living item, and insert after that.
When you get conflicting edits, create the set of all possible changes, and decide each one logically…
“Causal context” - what did this node see at the time this operation happened?
It seems like implementing this just for strings wouldn’t be too hard. And would be super cool. And then we could look again at the paper.
It’d be fun to do it in Haskell. I wonder could we use:
- Indexed monads to track states.
- Arrows to make using indexed monads more pleasant.
- Property-based tests to check the algorithm.
- A free monad for the computation that could eventually write out versions of the algorithm in different languages(?)
I want it to be so cheap to write correct software that we do more of it.
The goal of Idris is to reduce the cost of writing correct software.
Url: http://www.tinyurl.com/typedd Discount code: ctwcmeshType, Define, Refine
Energy usage scales linearly with the number of cores, but cubicly with the clock speed!
SSP - Stateful Stream Processing
- SSP is all about creating materialised views.
- From an infinite input.
- Either as a table, or as a stream.
https://kafka.apache.org https://hackage.haskell.org/package/haskakafka https://hackage.haskell.org/package/milena https://www.confluent.io/blog/bottled-water-real-time-integration-of-postgresql-and-kafka/ https://www.pipelinedb.com
Chandry-Lamport - https://en.wikipedia.org/wiki/Snapshot_algorithm CQRS - http://martinfowler.com/bliki/CQRS.html
- Streaming is a superset of ‘batch’.
- Separate the store and the view.
- Decentralized approaches are more general.
Part of atomist?
- [ ] Reason
- [ ] Fable :research:
- [ ] Bucklescript :research:
- [ ] Flare (Limited to certain use cases).
- [ ] Pux
- [ ] Thermite
- [ ] Halogen (It’s well supported and production-used, but haaard!)
- [ ] Optic UI
http://functorial.com/stack-safety-for-free/index.pdf
- [ ] Meta II
- [ ] Linda