diff --git a/._config.yml.~undo-tree~ b/._config.yml.~undo-tree~ new file mode 100644 index 0000000..9858df6 --- /dev/null +++ b/._config.yml.~undo-tree~ @@ -0,0 +1,13 @@ +(undo-tree-save-format-version . 1) +"58bff125b4fa2851574ae1d5ddea39da01519cf7" +[nil nil nil nil (25784 2748 693105 533000) 0 nil] +([nil nil ((" - jekyll/agda +" . 184) (t 25731 13391 947645 202000)) nil (25784 2748 693096 475000) 0 nil]) +([nil nil ((" +" . -223) (203 . 224) 184 (t 25784 2748 706419 913000)) nil (25784 3092 539381 615000) 0 nil]) +([nil nil ((214 . 219) ("-minifier" . 214) (undo-tree-id0 . -9) (undo-tree-id1 . -9)) nil (25784 9662 492295 704000) 0 nil]) +([nil nil ((" +" . -287) (273 . 288) 260 (t 25784 3092 544429 619000)) nil (25784 9666 665317 968000) 0 nil] [nil nil ((261 . 327) 260 (t 25784 3092 544429 619000)) ((" " . 261) (undo-tree-id0 . -65) (undo-tree-id1 . -65) (undo-tree-id2 . -65) (undo-tree-id3 . -65)) (25784 9662 491895 244000) 0 nil]) +([nil current ((284 . 288) (279 . 284) ("LICENSE" . 279)) nil (25784 9666 665309 125000) 0 nil]) +nil +nil diff --git a/.shell.nix.~undo-tree~ b/.shell.nix.~undo-tree~ new file mode 100644 index 0000000..5e81f1a --- /dev/null +++ b/.shell.nix.~undo-tree~ @@ -0,0 +1,53 @@ +(undo-tree-save-format-version . 1) +"523c7493ee2508bc1f1b95adc6e5631228e37c2a" +[nil nil nil nil (25784 9246 552220 825000) 0 nil] +([nil nil ((34 . 37) (18 . 34) (7 . 18) (4 . 7) (#(" " 0 1 (fontified t)) . -4) (undo-tree-id0 . -1) (#("=" 0 1 (fontified t)) . -5) (undo-tree-id1 . -1) (#(" " 0 1 (fontified t)) . -6) (undo-tree-id2 . -1) 7 (1 . 7) (t . -1)) nil (25784 9246 552217 80000) 0 nil]) +([nil nil ((37 . 38)) nil (25784 9246 552175 288000) 0 nil]) +([nil nil ((#(" " 0 2 (fontified nil)) . -53) (undo-tree-id10 . -2) (55 . 56) (52 . 55) (38 . 52) (37 . 38) (35 . 37) (#(" +" 0 1 (fontified t)) . -35) (undo-tree-id11 . -1) (undo-tree-id12 . -1) (#(" " 0 1 (fontified t)) . -36) (undo-tree-id13 . -1) (undo-tree-id14 . -1) (#(" " 0 1 (fontified t)) . -37) (undo-tree-id15 . -1) (undo-tree-id16 . -1) 38 (36 . 38) (#(" " 0 2 (fontified nil)) . 35) (undo-tree-id17 . -1) (undo-tree-id18 . -2) (undo-tree-id19 . -1) (undo-tree-id20 . -1) (37 . 38) (t 25784 9246 557023 909000)) nil (25784 9281 26107 507000) 0 nil]) +([nil nil ((#(" " 0 2 (fontified nil)) . -70) (undo-tree-id9 . -2) (72 . 73) (67 . 72) (55 . 67) (52 . 55) 38) nil (25784 9281 26088 217000) 0 nil]) +([nil nil ((77 . 82) (72 . 77) (#("h" 0 1 (fontified t)) . -72) (undo-tree-id3 . -1) (#(" +" 0 1 (fontified t)) . -73) (undo-tree-id4 . -1) (#(" " 0 1 (fontified t)) . -74) (undo-tree-id5 . -1) (#(" " 0 1 (fontified t)) . -75) (undo-tree-id6 . -1) (#(" " 0 1 (fontified t)) . -76) (undo-tree-id7 . -1) (#(" " 0 1 (fontified nil)) . -77) 78 (73 . 78) (72 . 73) (#("h" 0 1 (fontified t)) . -72) (undo-tree-id8 . -1) 73 (72 . 73) (67 . 72) 55) nil (25784 9281 26076 601000) 0 nil]) +([nil nil (39) nil (25784 9289 175461 447000) 0 nil]) +([nil nil ((38 . 49) (t 25784 9281 32556 286000)) nil (25784 9289 175453 849000) 0 nil]) +([nil nil ((#("pkgs" 0 4 (fontified t)) . 49) (undo-tree-id22 . 4) (t 25784 9289 180448 609000)) nil (25784 9293 378235 843000) 0 nil]) +([nil nil ((#("." 0 1 (fontified t)) . 49) (undo-tree-id21 . 1)) nil (25784 9293 378228 63000) 0 nil]) +([nil nil ((#(";" 0 1 (fontified t)) . -94) (undo-tree-id23 . -1) (undo-tree-id24 . -1) (undo-tree-id25 . -1) (undo-tree-id26 . -1) (undo-tree-id27 . -1) (undo-tree-id28 . -1) (undo-tree-id29 . -1) (undo-tree-id30 . -1) (undo-tree-id31 . -1) (undo-tree-id32 . -1) (undo-tree-id33 . -1) (undo-tree-id34 . -1) (undo-tree-id35 . -1) (undo-tree-id36 . -1) (undo-tree-id37 . -1) (undo-tree-id38 . -1) (undo-tree-id39 . -1) (undo-tree-id40 . -1) (undo-tree-id41 . -1) (undo-tree-id42 . -1) (undo-tree-id43 . -1) (undo-tree-id44 . -1) (undo-tree-id45 . -1) (undo-tree-id46 . -1) 95 (94 . 95) (t 25784 9293 393393 348000)) nil (25784 9299 441886 244000) 0 nil]) +([nil nil ((92 . 93) (t 25784 9299 446314 437000)) nil (25784 9304 469228 604000) 0 nil]) +([nil nil ((114 . 116) (112 . 114) (111 . 112) (99 . 111) (#("l" 0 1 (fontified t)) . -99) (undo-tree-id239 . -1) 100 (97 . 100) (95 . 97) (#(" " 0 2 (fontified nil)) . 94) (undo-tree-id240 . -2) (undo-tree-id241 . -2) (96 . 97) (93 . 96) (t 25784 9304 477249 281000) 92) nil (25784 9344 934497 505000) 0 nil]) +([nil nil ((#(" shellHook = '' + '' +" 0 2 (fontified t) 2 11 (fontified t face nix-attribute-face) 11 14 (fontified t) 14 15 (syntax-table (15) nix-string-type 39 fontified t face font-lock-string-face) 15 17 (fontified t face font-lock-string-face) 17 20 (fontified t face font-lock-string-face) 20 21 (fontified t syntax-table (15) nix-string-type 39 face font-lock-string-face) 21 22 (fontified t)) . 95) (undo-tree-id150 . 1) (undo-tree-id151 . -3) (undo-tree-id152 . -3) (undo-tree-id153 . -3) (undo-tree-id154 . -3) (undo-tree-id155 . -3) (undo-tree-id156 . -3) (undo-tree-id157 . -3) (undo-tree-id158 . -3) (undo-tree-id159 . -3) (undo-tree-id160 . -3) (undo-tree-id161 . -3) (undo-tree-id162 . -3) (undo-tree-id163 . -3) (undo-tree-id164 . -3) (undo-tree-id165 . -3) (undo-tree-id166 . -3) (undo-tree-id167 . -3) (undo-tree-id168 . -3) (undo-tree-id169 . -3) (undo-tree-id170 . -3) (undo-tree-id171 . -3) (undo-tree-id172 . -3) (undo-tree-id173 . -3) (undo-tree-id174 . -3) (undo-tree-id175 . -3) (undo-tree-id176 . -3) (undo-tree-id177 . -3) (undo-tree-id178 . -3) (undo-tree-id179 . -3) (undo-tree-id180 . -3) (undo-tree-id181 . -3) (undo-tree-id182 . -3) (undo-tree-id183 . -3) (undo-tree-id184 . -3) (undo-tree-id185 . -3) (undo-tree-id186 . -3) (undo-tree-id187 . -3) (undo-tree-id188 . -3) (undo-tree-id189 . -3) (undo-tree-id190 . -3) (undo-tree-id191 . -3) (undo-tree-id192 . -3) (undo-tree-id193 . -3) (undo-tree-id194 . -3) (undo-tree-id195 . -3) (undo-tree-id196 . -3) (undo-tree-id197 . -3) (undo-tree-id198 . -3) (undo-tree-id199 . -3) (undo-tree-id200 . -3) (undo-tree-id201 . -3) (undo-tree-id202 . -3) (undo-tree-id203 . -3) (undo-tree-id204 . -3) (undo-tree-id205 . -3) (undo-tree-id206 . -3) (undo-tree-id207 . -3) (undo-tree-id208 . -3) (undo-tree-id209 . -3) (undo-tree-id210 . -3) (undo-tree-id211 . -3) (undo-tree-id212 . -3) (undo-tree-id213 . -3) (undo-tree-id214 . -3) (undo-tree-id215 . -3) (undo-tree-id216 . -3) (undo-tree-id217 . -3) (undo-tree-id218 . -3) (undo-tree-id219 . -3) (undo-tree-id220 . -3) (undo-tree-id221 . -3) (undo-tree-id222 . -3) (undo-tree-id223 . -3) (undo-tree-id224 . -3) (undo-tree-id225 . -3) (undo-tree-id226 . -3) (undo-tree-id227 . -3) (undo-tree-id228 . -3) (undo-tree-id229 . -3) (undo-tree-id230 . -3) (undo-tree-id231 . -3) (undo-tree-id232 . -3) (undo-tree-id233 . -3) (undo-tree-id234 . -3) (undo-tree-id235 . -3) (undo-tree-id236 . -3) (undo-tree-id237 . -3) (undo-tree-id238 . -3) 98) nil (25784 9344 934475 573000) 0 nil]) +([nil nil ((#(" +" 0 1 (fontified t)) . 94) (undo-tree-id47 . -1) (undo-tree-id48 . -1) (undo-tree-id49 . -1) (undo-tree-id50 . -1) (undo-tree-id51 . -1) (undo-tree-id52 . -1) (undo-tree-id53 . -1) (undo-tree-id54 . -1) (undo-tree-id55 . -1) (undo-tree-id56 . -1) (undo-tree-id57 . -1) (undo-tree-id58 . -1) (undo-tree-id59 . -1) (undo-tree-id60 . -1) (undo-tree-id61 . -1) (undo-tree-id62 . -1) (undo-tree-id63 . -1) (undo-tree-id64 . -1) (undo-tree-id65 . -1) (undo-tree-id66 . -1) (undo-tree-id67 . -1) (undo-tree-id68 . -1) (undo-tree-id69 . -1) (undo-tree-id70 . -1) (undo-tree-id71 . -1) (undo-tree-id72 . -1) (undo-tree-id73 . -1) (undo-tree-id74 . -1) (undo-tree-id75 . -1) (undo-tree-id76 . -1) (undo-tree-id77 . -1) (undo-tree-id78 . -1) (undo-tree-id79 . -1) (undo-tree-id80 . -1) (undo-tree-id81 . -1) (undo-tree-id82 . -1) (undo-tree-id83 . -1) (undo-tree-id84 . -1) (undo-tree-id85 . -1) (undo-tree-id86 . -1) (undo-tree-id87 . -1) (undo-tree-id88 . -1) (undo-tree-id89 . -1) (undo-tree-id90 . -1) (undo-tree-id91 . -1) (undo-tree-id92 . -1) (undo-tree-id93 . -1) (undo-tree-id94 . -1) (undo-tree-id95 . -1) (undo-tree-id96 . -1) (undo-tree-id97 . -1) (undo-tree-id98 . -1) (undo-tree-id99 . -1) (undo-tree-id100 . -1) (undo-tree-id101 . -1) (undo-tree-id102 . -1) (undo-tree-id103 . -1) (undo-tree-id104 . -1) (undo-tree-id105 . -1) (undo-tree-id106 . -1) (undo-tree-id107 . -1) (undo-tree-id108 . -1) (undo-tree-id109 . -1) (undo-tree-id110 . -1) (undo-tree-id111 . -1) (undo-tree-id112 . -1) (undo-tree-id113 . -1) (undo-tree-id114 . -1) (undo-tree-id115 . -1) (undo-tree-id116 . -1) (undo-tree-id117 . -1) (undo-tree-id118 . -1) (undo-tree-id119 . -1) (undo-tree-id120 . -1) (undo-tree-id121 . -1) (undo-tree-id122 . -1) (undo-tree-id123 . -1) (undo-tree-id124 . -1) (undo-tree-id125 . -1) (undo-tree-id126 . -1) (undo-tree-id127 . -1) (undo-tree-id128 . -1) (undo-tree-id129 . -1) (undo-tree-id130 . -1) (undo-tree-id131 . -1) (undo-tree-id132 . -1) (undo-tree-id133 . -1) (undo-tree-id134 . -1) (undo-tree-id135 . -1) (undo-tree-id136 . -1) (undo-tree-id137 . -1) (undo-tree-id138 . -1) (undo-tree-id139 . -1) (undo-tree-id140 . -1) (undo-tree-id141 . -1) (undo-tree-id142 . -1) (undo-tree-id143 . -1) (undo-tree-id144 . -1) (undo-tree-id145 . -1) (undo-tree-id146 . -1) (undo-tree-id147 . -1) (undo-tree-id148 . -1) (undo-tree-id149 . -1)) nil (25784 9344 934375 208000) 0 nil]) +([nil nil ((nil rear-nonsticky nil 36 . 37) (#(" +" 0 1 (fontified nil)) . -2141) (34 . 2142) 9 (t 25784 9344 948738 964000)) nil (25784 9380 113478 487000) 0 nil]) +([nil nil ((#(" " 0 2 (fontified t)) . -35) (undo-tree-id242 . -2) (undo-tree-id243 . -2) (undo-tree-id244 . -2) (undo-tree-id245 . -2) (undo-tree-id246 . -2) (undo-tree-id247 . -2) (undo-tree-id248 . -2) (undo-tree-id249 . -2) (undo-tree-id250 . -2) (undo-tree-id251 . -2) (undo-tree-id252 . -2) 37 (34 . 37) 7) nil (25784 9380 113471 740000) 0 nil]) +([nil nil ((35 . 41) (#(" " 0 1 (fontified t)) . -35) (undo-tree-id253 . -1) (undo-tree-id254 . -1) (#(" " 0 1 (fontified t)) . -36) (undo-tree-id255 . -1) (undo-tree-id256 . -1) 37 (34 . 37) (t 25784 9380 118314 454000) 5) nil (25784 9410 150674 661000) 0 nil]) +([nil nil ((#("let" 0 3 (fontified t)) . 38) (undo-tree-id297 . -2) (t 25784 9410 164964 805000)) nil (25784 9422 502281 852000) 0 nil]) +([nil nil ((38 . 52)) nil (25784 9426 397695 841000) 0 nil] [nil nil ((#("in +" 0 2 (fontified t face nix-keyword-face) 2 3 (fontified t) 3 4 (fontified t)) . 35) (undo-tree-id257 . -2) (undo-tree-id258 . -2) (undo-tree-id260 . -2) (undo-tree-id262 . -2) (undo-tree-id264 . -2) (undo-tree-id266 . -2) (undo-tree-id268 . -2) (undo-tree-id270 . -2) (undo-tree-id272 . -2) (undo-tree-id274 . -2) (undo-tree-id276 . -2) (undo-tree-id278 . -2) (undo-tree-id280 . -2) (undo-tree-id282 . -2) (undo-tree-id284 . -2) (undo-tree-id286 . -2) (undo-tree-id288 . -2) (undo-tree-id290 . -2) (undo-tree-id292 . -2) (undo-tree-id294 . -2) (undo-tree-id296 . -2) 37) ((35 . 39) (t 25784 9418 684867 739000)) (25784 9418 673825 524000) 0 nil]) +([nil nil ((#("with pkgs" 0 1 (face nix-keyword-face fontified t) 1 4 (fontified t face nix-keyword-face) 4 9 (fontified t)) . 2164) (t 25784 9426 410780 491000)) nil (25784 9430 898372 649000) 0 nil]) +nil +([nil nil ((#(";" 0 1 (fontified t)) . 2164)) nil (25784 9430 898370 733000) 0 nil]) +([nil nil ((#(" " 0 1 (fontified t)) . 2164)) nil (25784 9430 898361 942000) 0 nil]) +([nil nil ((43 . 62) (#("pkgs" 0 4 (fontified t)) . 43) (t 25784 9430 913729 973000)) nil (25784 9458 363364 943000) 0 nil]) +([nil nil ((#("let + pkgs = import {}; +" 0 3 (fontified t face nix-keyword-face) 3 4 (fontified t) 4 6 (fontified t) 6 10 (fontified t face nix-attribute-face) 10 13 (fontified t) 13 19 (fontified t face nix-builtin-face) 19 20 (fontified t) 20 29 (fontified t face nix-constant-face) 29 33 (fontified t) 33 34 (fontified t)) . 1) (undo-tree-id298 . -30) (undo-tree-id299 . 4) (undo-tree-id300 . -31) (undo-tree-id301 . 3) (undo-tree-id302 . -32) (undo-tree-id303 . -4) (undo-tree-id304 . -30) (undo-tree-id305 . -30) (undo-tree-id306 . -30) (undo-tree-id307 . -30) (undo-tree-id308 . -30) (undo-tree-id309 . -30) (undo-tree-id310 . -30) (undo-tree-id311 . -30) (undo-tree-id312 . -30) (undo-tree-id313 . -30) (undo-tree-id314 . -30) (undo-tree-id315 . -30) (undo-tree-id316 . -30) (undo-tree-id317 . -30) (undo-tree-id318 . -30) (undo-tree-id319 . -30) (undo-tree-id320 . -30) (undo-tree-id321 . -30) (undo-tree-id322 . -30) (undo-tree-id323 . -30) (undo-tree-id324 . -30) (undo-tree-id325 . -30) (undo-tree-id326 . -30) (undo-tree-id327 . -30) 31) nil (25784 9458 363357 73000) 0 nil]) +([nil nil ((#("in " 0 2 (fontified t face nix-keyword-face) 2 3 (fontified t)) . 1) (t 25784 9458 369427 140000)) nil (25784 9460 212523 577000) 0 nil]) +([nil nil ((#("pkgs.hello" 0 10 (fontified t)) . 2171) (t 25784 9460 217407 70000)) nil (25784 9507 808136 469000) 0 nil]) +([nil nil ((nil rear-nonsticky nil 2179 . 2180) (#(" +" 0 1 (fontified nil)) . -2351) (2171 . 2352) 2170) nil (25784 9518 416082 799000) 0 nil] [nil nil ((nil rear-nonsticky nil 2171 . 2172) (nil fontified nil 2171 . 2172) (2171 . 2172) 2170) ((#("u" 0 1 (fontified nil rear-nonsticky nil)) . 2171) (nil rear-nonsticky t 2171 . 2172)) (25784 9507 808006 617000) 0 nil]) +([nil nil ((#(" +" 0 4 (fontified t) 4 5 (fontified t)) . 2167) (undo-tree-id331 . -3) (undo-tree-id332 . -5) (undo-tree-id333 . -3) (undo-tree-id334 . -4) (undo-tree-id335 . -4) (undo-tree-id336 . -3) (undo-tree-id337 . -3) (undo-tree-id338 . -3) 2170) nil (25784 9518 416337 593000) 0 nil]) +nil +([nil nil ((#(" " 0 4 (fontified t)) . 2315) (undo-tree-id339 . -3) (undo-tree-id340 . -3) (undo-tree-id341 . -4) (#(" " 0 4 (fontified t)) . 2297) (undo-tree-id342 . -4) (#(" " 0 4 (fontified t)) . 2275) (undo-tree-id343 . -4) (#(" " 0 4 (fontified t)) . 2256) (undo-tree-id344 . -4) (#(" " 0 4 (fontified t)) . 2238) (undo-tree-id345 . -4) (#(" " 0 4 (fontified t)) . 2225) (undo-tree-id346 . -4) (#(" " 0 3 (fontified t) 3 4 (fontified t rear-nonsticky t)) . 2171) (undo-tree-id347 . -4)) nil (25784 9523 261623 469000) 0 nil] [nil nil ((#(" " 0 5 (fontified t)) . 2308) (undo-tree-id328 . -4) (undo-tree-id329 . -4) (undo-tree-id330 . -4) (#(" " 0 5 (fontified t)) . 2291) (#(" " 0 5 (fontified t)) . 2270) (#(" " 0 5 (fontified t)) . 2252) (#(" " 0 5 (fontified t)) . 2235) (#(" " 0 5 (fontified t)) . 2223) (#(" " 0 4 (fontified t) 4 5 (fontified t rear-nonsticky t)) . 2170) 2342) ((2170 . 2175) (2223 . 2228) (2235 . 2240) (2252 . 2257) (2270 . 2275) (2291 . 2296) (2308 . 2313)) (25784 9518 416066 262000) 0 nil]) +([nil nil ((#("with " 0 4 (fontified t face nix-keyword-face) 4 5 (fontified t)) . 2204) (t 25784 9523 278744 484000)) nil (25784 9561 336027 219000) 0 nil]) +nil +([nil nil ((#("rubygems" 0 8 (fontified t)) . 2204)) nil (25784 9561 336024 959000) 0 nil]) +([nil nil ((#(";" 0 1 (fontified t)) . 2204)) nil (25784 9561 336023 660000) 0 nil]) +([nil nil ((#(" " 0 1 (fontified t)) . 2204)) nil (25784 9561 336016 82000) 0 nil]) +([nil nil ((#(" " 0 1 (fontified t)) . -127) (undo-tree-id348 . -1) (undo-tree-id349 . -1) (undo-tree-id350 . -1) (undo-tree-id351 . -1) (undo-tree-id352 . -1) (undo-tree-id353 . -1) (undo-tree-id354 . -1) (undo-tree-id355 . -1) (undo-tree-id356 . -1) (undo-tree-id357 . -1) (undo-tree-id358 . -1) (undo-tree-id359 . -1) (undo-tree-id360 . -1) (undo-tree-id361 . -1) (undo-tree-id362 . -1) (undo-tree-id363 . -1) (undo-tree-id364 . -1) (undo-tree-id365 . -1) (undo-tree-id366 . -1) (undo-tree-id367 . -1) (undo-tree-id368 . -1) (undo-tree-id369 . -1) (undo-tree-id370 . -1) 128 (119 . 128) (#("c" 0 1 (fontified t)) . -119) (undo-tree-id371 . -1) (#("a" 0 1 (fontified t)) . -120) (undo-tree-id372 . -1) 121 (114 . 121) (t 25784 9561 351364 64000)) nil (25784 9587 142689 414000) 0 nil]) +([nil current ((2184 . 2190) (2179 . 2184) (t 25784 9587 159113 922000) 2178) nil (25784 9646 114392 527000) 0 nil]) +nil diff --git a/_config.yml b/_config.yml index c5b94c0..6712969 100644 --- a/_config.yml +++ b/_config.yml @@ -5,13 +5,14 @@ title: "rachel.cafe" # the name of your site, e.g. ACME Corp. plugins: - jekyll-feed - jekyll-katex - - jekyll/agda - jekyll-minifier + - jekyll/agda exclude: - "*.agdai" - "readme.md" - "LICENSE" + - "shell.nix" katex: rendering_options: diff --git a/_drafts/.the-algebra-in-algebraic-datatypes.md.~undo-tree~ b/_drafts/.the-algebra-in-algebraic-datatypes.md.~undo-tree~ new file mode 100644 index 0000000..ef0599d --- /dev/null +++ b/_drafts/.the-algebra-in-algebraic-datatypes.md.~undo-tree~ @@ -0,0 +1,4 @@ +(undo-tree-save-format-version . 1) +"14b4fac3fb89459c858bfc19e2649db580c097ce" +[nil current nil nil (25784 9131 42808 229000) 0 nil] +nil diff --git a/_drafts/haskell-in-a-category.md b/_drafts/haskell-in-a-category.md deleted file mode 100644 index 3d66a67..0000000 --- a/_drafts/haskell-in-a-category.md +++ /dev/null @@ -1,10 +0,0 @@ ---- -layout: post -title: "Haskell, Categories and Algebra" ---- - -some general stuff about haskell and categories as well as algebraic datatypes, F-algebras and some concrete examples of fixpoint constructions and catamorphisms - - - - diff --git a/_drafts/the-algebra-in-algebraic-datatypes.md b/_drafts/the-algebra-in-algebraic-datatypes.md new file mode 100644 index 0000000..0c0d67a --- /dev/null +++ b/_drafts/the-algebra-in-algebraic-datatypes.md @@ -0,0 +1,62 @@ +--- +layout: post +title: "The algebra in algebraic datatypes" +--- + +In this post I will explore the algebraic properties of Haskell's types, give an informal description of category theory, F-algebras, homomorphisms, catamorphisms and a roundabout way to write a `foldr` that recurses backwards. + + + +# Algebra on types in Haskell +* Basic algebraic properties + * Products, Either, Functions + * Non-recursive datatypes + * Algebraic equivalences over types + +# Thinking with functions +* Towards category theory + * Initial objects + * Generalized elements + +# From functions to morphisms +* What is a category? + * All about morphisms + * Explain commuting diagrams somewhere here? + * Products + * Sums + * Exponents + +# Functors in category theory +* Functors + * Endofunctors + +# Algebra through functors +* Algebra in a category + * Monoidal object + * Use this to motivate F-algebras + * Homomorphism + * relate to classical concept of homomorphisms + * some examples + +# Datatypes through fixpoints +* Recursive types in haskell as fixpoints of functors + * Initial algebra fixpoints + * Construction + * Catamorphisms + * Some examples of familiar datatypes described in this way + * How catamorphisms compute backwards + +# Writing foldr +* Recovering `foldr` + +# ??? +* Recommendations + * Category theory for programmers + * Ther are many category theory books + +# Bonus: monoids in the category of endofunctors +* monads are monoids in the category of endofunctors + * category of endofunctors + * natural transformations + * relate monoid example from before + * multiplication given by composition instead of $\times$ diff --git a/_layouts/.default.html.~undo-tree~ b/_layouts/.default.html.~undo-tree~ new file mode 100644 index 0000000..aaa653f --- /dev/null +++ b/_layouts/.default.html.~undo-tree~ @@ -0,0 +1,4 @@ +(undo-tree-save-format-version . 1) +"b4678c7c50ca2382a4ee19802e15ad4b121d22a9" +[nil current nil nil (25733 45126 379234 704000) 0 nil] +nil diff --git a/shell.nix b/shell.nix new file mode 100644 index 0000000..4c4f61b --- /dev/null +++ b/shell.nix @@ -0,0 +1,92 @@ +with import {}; let + + json-minify = (buildRubyGem { + gemName = "json-minify"; + dependencies = [ rubyPackages.json ]; + groups = ["default"]; + platforms = []; + source = { + remotes = ["https://rubygems.org"]; + sha256 = "fd38ef93867332c2340aaf1b57335782ab5958fe6fb3ca7a8aba1469f0bf08ae"; + type = "gem"; + }; + version = "0.0.3"; + }); + + htmlcompressor = (buildRubyGem { + gemName = "htmlcompressor"; + dependencies = [ ]; + groups = ["default"]; + platforms = []; + source = { + remotes = ["https://rubygems.org"]; + sha256 = "4630cf8ed46b563f0b49cc6028a3fe8c17a9067f2becd7c3a2aa5aaacefb1f9e"; + type = "gem"; + }; + version = "0.4.0"; + }); + + cssminify2 = (buildRubyGem { + gemName = "cssminify2"; + dependencies = [ ]; + groups = ["default"]; + platforms = []; + source = { + remotes = ["https://rubygems.org"]; + sha256 = "e311cfced4ccfc55d27bf30520f7d11ed129bf04dcadd5a82e791a141e45b98c"; + type = "gem"; + }; + version = "2.0.1"; + }); + + jekyll-katex = (buildRubyGem { + gemName = "jekyll-katex"; + dependencies = [ rubyPackages.execjs jekyll ]; + groups = ["default"]; + platforms = []; + source = { + remotes = ["https://rubygems.org"]; + sha256 = "ff16aced6a4577a76bf429c853a055ff6511a06f8fee06028adc26aaf28f58cd"; + type = "gem"; + }; + version = "1.0.0"; + }); + + jekyll-minifier = (buildRubyGem { + gemName = "jekyll-minifier"; + dependencies = [ cssminify2 htmlcompressor rubyPackages.jekyll json-minify rubyPackages.uglifier ]; + groups = ["default"]; + platforms = []; + source = { + remotes = ["https://rubygems.org"]; + sha256 = "cd05bd9b2105f1dfd344397c480c17bea7d93871e239f5ca3949852ff1d938a3"; + type = "gem"; + }; + version = "0.1.10"; + }); + + jekyll-agda = (buildRubyGem { + gemName = "jekyll-agda"; + dependencies = [ agda jekyll ]; + groups = ["default"]; + platforms = []; + source = { + remotes = ["https://rubygems.org"]; + sha256 = "fb2af6ac3ce9f11260b1c3d8e28075f23436577e5172e7defa029fb90e808fa3"; + type = "gem"; + }; + version = "0.1.0"; + }); +in +mkShell { + packages = [ + nodejs + (ruby.withPackages (ps: with ps; [ + jekyll + jekyll-feed + jekyll-katex + jekyll-minifier + jekyll-agda + ])) + ]; +}