| module MathInterpreter (mathInterpreter) where | |
| import Data.Char | |
| data Token = Number Integer | |
| | Plus | |
| | Dash | |
| | Star | |
| | Slash | |
| deriving Show |
| +-assoc-proof : ∀ (x y z : ℕ) → x + (y + z) ≡ (x + y) + z | |
| +-assoc-proof zero y z = refl | |
| +-assoc-proof (suc x) y z = cong suc (+-assoc-proof x y z) |
| with recursive fib as ( | |
| select 0 as a, 1 as b | |
| union | |
| select b, a + b from fib | |
| ) select a from fib limit 5; |
| type Iter<A> = () => A | null; | |
| const array_to_iter = <A>(arr: A[]): Iter<A> => { | |
| let index = 0; | |
| return () => { | |
| const el = arr[index]; | |
| index += 1; | |
| return el; | |
| } |
When working on relational databases there are some guarantees called ACID, but these guarantees are not as safe as we usually think.
Let's start with a simple situation, imagine that you have a system that holds a balance of each user in some SQL database.
| user A | user B |
|---|---|
| id: 1 | id: 2 |
| balance: 100 | balance: 50 |
| const useState = <A>(a: any): any => { }; | |
| type Tree = [number, Tree, Tree] | null | |
| type UUID = string; | |
| type Edge = { from: UUID, to: UUID } | |
| type NNode = { nodes: NNode[], id: UUID, label: string } | |
| const [nodes, setNodes] = useState<NNode | null>(null); |
| module Main | |
| import Network.Socket.Data | |
| data Fin : Nat -> Type where | |
| FZ : Fin (S k) | |
| FS : Fin k -> Fin (S k) | |
| Show (Equal x y) where | |
| show _ = "Equality" |
| <html> | |
| <body> | |
| <style contenteditable> | |
| style { display: block; }@keyframes animat { 0% { background-color: pink; } 50% { background-color: orange; } 100% { background-color: red; } }body { animation: animat 750ms infinite alternate; } | |
| </style> | |
| </body> | |
| </html> |
| /** | |
| * Evaluates an expression in Reverse Polish Notation. | |
| * | |
| * @param {string} expression - The input expression. | |
| * @returns {number} The result of the RPN expression. | |
| */ | |
| // This script parses the expression into a tree and then evaluates, should be something like O(n) because iterates once on the parsing and once in the evaluating | |
| type Operator = {op: string, left: Operator | number, right: Operator | number}; |
| /** | |
| * Finds the number in an array with the most digits. | |
| * | |
| * @param {string} signals - The incomplete source. | |
| * @returns {string[]} Suggestions of possible complete sources. | |
| */ | |
| const MORSE_DICTIONARY: Record<string, string> = { | |
| ".": "E", | |
| "-": "T", |
