Created
October 7, 2025 07:45
-
-
Save qexat/147c99ecbb71ce8469f7d84fa087cf7e to your computer and use it in GitHub Desktop.
functor ramblings in pseudo-haskell. unfortunately perfect parsing requires multicategories
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| e ::= x | |
| | '(' e ')' | |
| | e e | |
| | 'λ' x '.' e | |
| --------------------------------------------------------------- | |
| _&>_ a b = a ∧ (a → b) | |
| or_elim = (a → c) → (b → c) → a ∨ b → c | |
| or_elim f _ (Left a) = f a | |
| or_elim _ g (Right b) = g b | |
| map₃ : (a → b → c → d) → Maybe a → Maybe b → Maybe c → Maybe d | |
| map₃ f x y z = bind (map2 f x y) (flip map z) | |
| branch : Maybe (a → c) → Maybe (b → c) → Maybe (a ∨ b) → Maybe c | |
| branch = map₃ or_elim | |
| and_then_elim₁ : (a &> b) → a | |
| and_then_elim₁ (a, _) = a | |
| and_then_elim₂ : (a &> b) → b | |
| and_then_elim₂ (a, b) = b a | |
| uncurry : (a → b → c) → (a &> b) → c | |
| uncurry f₂ (a, a_to_b) = f₂ a (a_to_b a) | |
| unnamed_1 : Maybe (a &> b) → Maybe a | |
| unnamed_1 = map and_then_elim₁ | |
| unnamed_2 : Maybe (a &> b) → Maybe b | |
| unnamed_2 = map and_then_elim₂ | |
| -- uncurried variant of Applicative's apply₂, except that instead of a ∧ b | |
| -- we have the ordered (dependent?) sum a &> b, because we don't want to engage | |
| -- with the rest of the grammar rule if what we got so far isn't what we expected | |
| -- | |
| -- e.g. when parsing an application we expect a and b to be expressions, but if | |
| -- a is something else then there is no point in even considering parsing that rule | |
| unnamed_3 : Maybe (a → b → c) → Maybe (a &> b) → Maybe c | |
| unnamed_3 = map₂ uncurry |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment