A categorical programming language
| 修订版 | 7353729e238c5dac3466d91ae8b84594367e9caa (tree) |
|---|---|
| 时间 | 2022-04-15 10:20:34 |
| 作者 | Corbin <cds@corb...> |
| Commiter | Corbin |
Add beta-uncurry rule.
hive/monads/int-lift.cammy (diff) hive/v2/dual/about.md (diff) hive/v2/dual/e.cammy (diff) hive/v2/dual/mul.cammy (diff) jelly/src/main.rs (diff)| @@ -0,0 +1,3 @@ | ||
| 1 | +(fun/postcomp @0) | |
| 2 | + | |
| 3 | +Lift an internal hom to a monad, given the unit of the monad. |
| @@ -0,0 +1,2 @@ | ||
| 1 | +Pairs of numbers can be interpreted as [dual | |
| 2 | +numbers](https://en.wikipedia.org/wiki/Dual_number). |
| @@ -0,0 +1,3 @@ | ||
| 1 | +(pair f-zero f-one) | |
| 2 | + | |
| 3 | +The epsilon unit. |
| @@ -0,0 +1,7 @@ | ||
| 1 | +(pair | |
| 2 | + (f/mulpair (comp fst fst) (comp snd fst)) | |
| 3 | + (f/addpair | |
| 4 | + (f/mulpair (comp fst fst) (comp snd snd)) | |
| 5 | + (f/mulpair (comp fst snd) (comp snd fst)))) | |
| 6 | + | |
| 7 | +Multiplication in the dual numbers. |
| @@ -87,6 +87,8 @@ fn main() -> std::io::Result<()> { | ||
| 87 | 87 | |
| 88 | 88 | // Cousineau, Curien, & Mauny 1987 |
| 89 | 89 | rw!("beta"; "(comp (pair (curry ?x) ?y) (uncurry id))" => "(comp (pair id ?y) ?x)"), |
| 90 | + // beta when ?x is (uncurry ...) | |
| 91 | + rw!("beta-uncurry"; "(comp (pair ?x ?y) (uncurry id))" => "(comp (pair id ?y) (uncurry ?x))"), | |
| 90 | 92 | |
| 91 | 93 | rw!("nat-elim-pr"; "(pr zero succ)" => "id"), |
| 92 | 94 | rw!("nat-unroll-pr-zero"; "(comp zero (pr ?x ?f))" => "?x"), |
Fork