AlBasmala:
Blogging with Emacs & Org-mode (•̀ᴗ•́)و

[
  {
    "file": "java-cheat-sheet",
    "title": "Java CheatSheet",
    "date": "2023-12-25 Mon",
    "image": "modern-java.png 88% 88%",
    "description": "Quick reference for an old-school-cool high-level language ^_^",
    "tags": "java cheat-sheet",
    "url": "https://alhassy.com/java-cheat-sheet",
    "history": "https://github.com/alhassy/alhassy.github.io/commits/master/posts/java-cheat-sheet.org",
    "abstract": "\n#+begin_center\n#+html: This is a quick reference of concepts in modern Java.\n\nbadge:PDF|colorful_cheat_sheet|success|https://alhassy.com/java-cheat-sheet.pdf|read-the-docs\n\n# badge:license|GNU_3|informational|https://www.gnu.org/licenses/gpl-3.0.en.html|read-the-docs\ntweet:https://alhassy.com/java-cheat-sheet\nbadge:|buy_me_a_coffee|gray|https://www.buymeacoffee.com/alhassy|buy-me-a-coffee\nbadge:contributions|welcome|green|https://github.com/alhassy/alhassy.github.io/issues\n# badge:author|musa_al-hassy|purple|https://alhassy.github.io/|nintendo-3ds\n# badge:Warning|Incomplete_DRAFT|red||codeigniter\n#+end_center\n\n# @@html: <br> @@\n\nModern Java is a strongly-typed, eagery evaluated, case sensative, yet\nwhitespace insensative language. It uses hierarchies of classes/types\nto structure data, but also has first-class support for\nfunctional-style algebraic datatypes.\n\nJava programs are made up of ‘classes’, classes contain methods, and methods contain commands.  To just try out a\nsnippet of code, we can\n+ Open a terminal and enter ~jshell~; then enter:\n     #+begin_src java\n1 + 2 // The jshell lets you try things out!\n\n// Say hello in a fancy way\nimport javax.swing.*;\nJOptionPane.showMessageDialog(new JFrame(), \"Hello, World!\");\n\n#+end_src\n\n+ Alternatively, in IntelliJ, click /Tools/ then /Groovy Console/ to try things out!\n+ Finally, [[http://alhassy.com/making-vscode-itself-a-java-repl.html][VSCode]] allows arbitrary Java code to be sent to a ~jshell~\n  in the background(!) and it echoes the result in a friendly way.\n\n# A program cannot consist of only commands. Java commands must be inside functions, and functions must be inside classes.\n#\n# Imagine a sofa. A sofa cannot exist on its own. It exist in a room somewhere. And a room also cannot exist on its own. A room is located in some house. Or, you could say that the house is divided into rooms, and those rooms contain things.\n#\n# Java programs are made up of classes, classes contain methods, and methods contain commands.\n\n# A minimal program must consist of at least one class, which must have at least\n# one method (function) that marks the program's starting point. This method must\n# be named main.\n\n:MWE:\nIn order to run a java program, it must have a main method as an entry point.\n\n#+begin_src java\n  public class LearnJava {\n      // In order to run a java program, it must have a main method as an entry\n      // point.\n      public static void main(String[] args) {\n          System.out.println(\"Hello World!\");\n\n          // Use System.out.printf() for easy formatted printing.\n          System.out.printf(\"pi = %.5f\", Math.PI); // => pi = 3.14159\n      }\n  }\n#+end_src\n:End:\n\n** Web reference                                                     :ignore:\n\n#+macro: begin-ignore-html #+html: <!--\n#+macro: end-ignore-html #+html: -->\n\n#+latex: \\vspace{-1em}\n{{{begin-ignore-html()}}}\nTo be terse, lots of content is not shown in this [[http://alhassy.com/java-cheat-sheet.pdf][PDF]], but is shown in the *[[https://alhassy.com/java-cheat-sheet][HTML]]*\nversion.\n{{{end-ignore-html()}}}\n"
  },
  {
    "file": "repl-driven-development",
    "title": "💐 Repl Driven Development: /Editor Integrated REPLs for all languages/ 🔁",
    "date": "2023-09-08 Fri",
    "image": "rdd-benefits.png",
    "description": "Press “C-x C-e” to send any piece of code (in any language) to a REPL in the background, within Emacs!",
    "tags": "repl-driven-development vscode emacs javascript java python lisp clojure haskell arend purescript idris racket",
    "url": "https://alhassy.com/repl-driven-development",
    "history": "https://github.com/alhassy/alhassy.github.io/commits/master/posts/repl-driven-development.org",
    "abstract": "\n#+begin_center\nbadge:Warning|Incomplete_DRAFT|red||codeigniter\n#+end_center\n\nThe melpa:repl-driven-development package makes the philosophy of REPL Driven\nDevelopment (RDD) accessible to any language that has a primitive CLI repl: /The\nresult is an Emacs interface for the language, where code of your choosing is/\n/evaluated, and results are echoed at your cursor in overlays./\n\nThat is, with Repl *green:aided* development, you make software by starting with\nan already working program (i.e., the repl) then *green:incrementlly* “teach it”\nto be the program you want, by defining & redefining things.  Until satisfied,\nloop: Type/modify code *[[green:in your editor]]*, press some keys to evaluate what you\nwrote/modified /in the currently running system/, and explore/test the resulting\nruntime.\n# Eventually, save your code as a clean text file.\n\n/RDD is programming emphasising fast & rich feedback from a running system./ RDD\nis fantastic for quickly /teaching/exploring/ an idea; as such, the running\nexample of this article will be on servers ---no prior experience with servers\nis assumed.\nThe main examples will be in JavaScript, Python, and Java.  (Since /JavaScript is\njust Lisp in C clothing/, we will not discuss Lisp.)  Since Java is verbose, the\npower of REPLs really pays off when exploring a new idea. We see how many\nimports and setup-code simply disappear in the RDD approach, letting you focus\non the core idea you're exploring/teaching.  For comparison, a traditional\nself-contained Java server program is ~30 lines long whereas the focused RDD\napproach is ~4 lines long.\n#\n# + We begin with JavaScript: Write some code, and see it interact with your browser.\n# + Then Python: Write some code, and see it interact with the terminal.\n\n# badge:repl-driven-development|1.4|informational|https://github.com/alhassy/repl-driven-development|Gnu-Emacs\n\n#+begin_center\nbadge:license|GNU_3|informational|https://www.gnu.org/licenses/gpl-3.0.en.html|read-the-docs\ntweet:https://alhassy.com/repl-driven-development\nbadge:|buy_me_a_coffee|gray|https://www.buymeacoffee.com/alhassy|buy-me-a-coffee\n@@TODO: FIX contributions URL@@\nbadge:contributions|welcome|green|https://github.com/alhassy/alhassy.github.io/issues\n#+end_center\n\n# @@html: <br> @@\n\n/tdlr:/ This library provides the Emacs built-in kbd:C-x_C-e behaviour for\narbitrary languages, provided they have a primitive cli REPL.\n"
  },
  {
    "file": "arabic-cheat-sheet",
    "title": "Arabic CheatSheet",
    "date": "2023-06-14 Wed",
    "image": "arabic-irab.png 100% 100%",
    "description": "Quick reference for the Arabic language; Modern Standard Arabic",
    "tags": "arabic cheat-sheet",
    "url": "https://alhassy.com/arabic-cheat-sheet",
    "history": "https://github.com/alhassy/alhassy.github.io/commits/master/posts/arabic-cheat-sheet.org",
    "abstract": "\n#+latex: \\iffalse\n\n#+begin_center\n#+html: This is a quick reference of concepts in the Arabic language.\n\nbadge:PDF|colorful_cheat_sheet|success|https://alhassy.com/arabic-cheat-sheet.pdf|read-the-docs\n\n# badge:license|GNU_3|informational|https://www.gnu.org/licenses/gpl-3.0.en.html|read-the-docs\ntweet:https://alhassy.com/arabic-cheat-sheet\nbadge:|buy_me_a_coffee|gray|https://www.buymeacoffee.com/alhassy|buy-me-a-coffee\n#+end_center\n\n# @@html: <br> @@\n\n#+latex: \\fi\n"
  },
  {
    "file": "family-tree",
    "title": "My Family Tree",
    "date": "2023-02-02 Thu",
    "image": "../images/family-tree.png 88% 88%",
    "description": "من هو في شجرة العائلة القديمة",
    "tags": "family",
    "url": "https://alhassy.com/family-tree",
    "history": "https://github.com/alhassy/alhassy.github.io/commits/master/posts/family-tree.org",
    "abstract": "\n#+begin_center\nbadge:Warning|Incomplete_DRAFT|red||codeigniter\n#+end_center\n\nWho's who in the old family tree\n"
  },
  {
    "file": "karate",
    "title": "A Brisk Introduction to Karate",
    "date": "2023-02-02 Thu",
    "image": "https://www.usadojo.com/wp-content/uploads/2013/08/Goju-Ryu-Karate-600x300.png 88% 88%",
    "description": "Discovering what be ka-ra-te",
    "tags": "karate",
    "url": "https://alhassy.com/karate",
    "history": "https://github.com/alhassy/alhassy.github.io/commits/master/posts/karate.org",
    "abstract": "\n#+begin_center\nbadge:Warning|Incomplete_DRAFT|red||codeigniter\n#+end_center\n\nWhat are the basic forms of Karate? What is Karate?\n\n/“The ultimate aim of karate lies not in victory or defeat but in the perfection\nof the character of its participants … to subdue the enemy without fighting is/\n/the highest skill, know your enemy and know yourself, in a hundred battles you\nwill not be defeated”/ says Gichin Funakoshi ---known as The Father of Modern Karate.\n\n/Karate/ means “empty hand” and was developed on the island of Okinawa ---part of\nmodern-day Japan.  The major styles (“Ryu”) are Shotokan, Wado-ryu,\nShito-ryu, and Goju-ryu ---many other styles of Karate are derived from these\nfour. I'm focusing on Goju-Ryu in this article: Goju-Ryu was founded by Chojun\nMiyagi; whose colleague, Gichin Funakosi, founded Shotokan-Ryu.\n\n#+begin_center\nimage:http://www.traditionalshotokankarate.co.uk/kara-te-do.gif\n#+end_center\n\nOccasionally one sees /Karate-Do/, which means “the way of the empty hand”.\nThis usage is a reminder that Karate is not just about fighting, but is also\na spiritual discipline.\n\nThe basic form of Goju-Ryu karate is Sanchin, “3 battles”: The battles of the\nmind, the body, and the spirit.  However, this was considered a bit difficult\nfor beginners, and so new forms were needed as a way of introducing fundamental\nkarate forms to a wider audience.  There are the “peaceful and safe” forms known\nas Pinan/Heian, the “first course” or Taikyoku forms, the “popularising forms”\nknown as Fukyugata ---the second of which was rebranded as “attack & smash”,\nGekaisai--- and, finally, there is the so-called Dachi-waza form. This last one\nis relatively new, and aims to be a smooth introduction to the world of\nforms/Kata.\n\nIn this article, I'd like to discuss the basic forms and their relationships.\n#+begin_center\nimage:https://www.sullivanskarateschool.com/wp-content/uploads/2019/07/saifa.gif\n#+end_center\n"
  },
  {
    "file": "arabic-word-order",
    "title": "A Brisk Introduction to the Fundamentals of Arabic Grammar, نحو",
    "date": "2022-11-03 Thu",
    "image": "arabic-irab.png 100% 100%",
    "description": "Discovering how to say “a/an/the” in Arabic leads onto a zany adventure into case markings, gender, annexation, non-verbal sentences, plurals, and concludes with whether “Muslims” is مسلمون or مسلمین ---it's both!",
    "tags": "arabic",
    "url": "https://alhassy.com/arabic-word-order",
    "history": "https://github.com/alhassy/alhassy.github.io/commits/master/posts/arabic-word-order.org",
    "abstract": "\n# I'd like to discuss the importance of Arabic's short vowels and their use to give Arabic flexible word order.\n\nIn short: In English sometimes we mess-up between “I/me/my”, likewise in Arabic we might mess up with “ابو / ابا / ابي”:\nThese are just اب followed by one of ا/ي/و (which are the pronounced case endings!)\n\n#+begin_center\n~ ~ ~ ~ ~ ~ ~\n#+end_center\n\n How do Arabs say the English “a/an/the”, as in “an apple” or “the chair”? Easy! By default, all words are /indefinite/\n (“a/an”); and made /definite/ (“the”) by adding الـ to the front of the word.\n\n But... there's some subtleties, which first require us to discuss vowel markings... which also change if the /feminine\n marker/ ة is used, so we also need to briefly discuss gender.\n\nEnglish relies on /word order/ for meaning; for example, /Jim hit Bob/ is a sentence where the person doing the action is\n/Jim/ and we know it has to be /Jim/, and not /Bob/, since /Jim/ is the word /before/ the action /hit/. However, in Arabic words can\nbe ordered in almost any way you like! Then how do we identifiy who does an action? We use *[[green:case markings]]*: We add small\nsymbols to the end of words to indiciate the role they play in a sentence.\n\nWith vowel markings, we can finally flesh-out the nature of\n“a/an/the” in Arabic... but then something wild happens if we stick\nan (in)definite /followed by/ a definite! We get the concepts of ownership and complete sentences that don't need a verb!\n\nFinally, we conclude with an explanation of why in the world English Qurans use the single word /muslim/ where's Arabic\nQurans use both مسلمون and مسلمين.\n"
  },
  {
    "file": "arabic-roots",
    "title": "Arabic Roots: The Power of Patterns",
    "date": "2022-11-02 Wed",
    "image": "https://unsplash.com/photos/Ejdemp9O7Po",
    "description": "Let's learn about how the Arabic language makes use of “roots” to obtain various words",
    "tags": "arabic javascript emacs",
    "url": "https://alhassy.com/arabic-roots",
    "history": "https://github.com/alhassy/alhassy.github.io/commits/master/posts/arabic-roots.org",
    "abstract": "\nI want to quickly introduce the Arabic language, through its “root system” ---i.e., most words have 3-letters at their\ncore--- and how these roots can be placed in “patterns” to obtain new words.\n\nI'd like to take a glance at Arabic's Verb Forms: These give you 10 words for each root!\n\nSome *green:interesting* concepts will also be mentioned, for those curious, but should be ignored on a first\nreading. These will be hidden away in /clickable/foldable/ regions.\n\nThese are notes of things that I'm learning; there's likely errors.\n"
  },
  {
    "file": "arabic-glossary",
    "title": "Glossary of Arabic Linguistic Terms",
    "date": "2022-11-01 Tue",
    "image": "arabic-irab.png 100% 100%",
    "description": "Definitions, and discussions, of jargon relating to learning the Arabic language.",
    "tags": "arabic",
    "url": "https://alhassy.com/arabic-glossary",
    "history": "https://github.com/alhassy/alhassy.github.io/commits/master/posts/arabic-glossary.org",
    "abstract": "Definitions, and discussions, of jargon relating to learning the Arabic language."
  },
  {
    "file": "cartoon",
    "title": "Arabic Cartoons",
    "date": "2022-10-21 Fri 11:20",
    "image": "https://upload.wikimedia.org/wikipedia/en/6/64/Dora_and_Boots.jpg 350 300",
    "description": "A simple interface to watch the engaging Arabic cartoons",
    "tags": "family arabic javascript",
    "url": "https://alhassy.com/cartoon",
    "history": "https://github.com/alhassy/alhassy.github.io/commits/master/posts/cartoon.org",
    "abstract": "\nA simple interface to watch the engaging Arabic cartoons.\n"
  },
  {
    "file": "making-vscode-itself-a-java-repl",
    "title": "💐 Making VSCode itself a Java REPL 🔁",
    "date": "2022-09-05 Mon",
    "image": "https://github.com/alhassy/easy-extensibility/blob/main/graphics/repl-java.gif?raw=true 90% 90%",
    "description": "VSCode evaluates Java code wherever it sees it, by sending it to a JShell in the background, and echos the results in a friendly way!",
    "tags": "repl-driven-development vscode emacs javascript java python ruby clojure typescript haskell lisp",
    "url": "https://alhassy.com/making-vscode-itself-a-java-repl",
    "history": "https://github.com/alhassy/alhassy.github.io/commits/master/posts/making-vscode-itself-a-java-repl.org",
    "abstract": "\nVSCode evaluates Java code wherever it sees it, by sending it to a JShell in the background, and echos the results in a\nfriendly way!\n\nThis is achieved with a [[https://github.com/alhassy/easy-extensibility][meta-extension for VSCode]] that makes VSCode into a living, breathing, JS interpreter: It can\nexecute arbitrary JS that alters VSCode on-the-fly.  /(Inspired by using Emacs and Lisp!)/\n\nThe relevant docs show how to make a similar REPL for [[https://github.com/alhassy/easy-extensibility/blob/65572a283e4864d9bef157b438c33f4e47276e3a/vscodejs/index.js#L1417-L1420][Python]], [[https://github.com/alhassy/easy-extensibility/blob/65572a283e4864d9bef157b438c33f4e47276e3a/vscodejs/index.js#L1459-L1462][Ruby]], [[https://github.com/alhassy/easy-extensibility/blob/65572a283e4864d9bef157b438c33f4e47276e3a/vscodejs/index.js#L1475-L1479][Clojure]], [[https://github.com/alhassy/easy-extensibility/blob/65572a283e4864d9bef157b438c33f4e47276e3a/vscodejs/index.js#L1490-L1494][Common Lisp]], [[https://github.com/alhassy/easy-extensibility/blob/65572a283e4864d9bef157b438c33f4e47276e3a/vscodejs/index.js#L1509-L1515][JavaScript]], [[https://github.com/alhassy/easy-extensibility/blob/65572a283e4864d9bef157b438c33f4e47276e3a/vscodejs/index.js#L1527-L1536][Typescript]],\n[[https://github.com/alhassy/easy-extensibility/blob/65572a283e4864d9bef157b438c33f4e47276e3a/vscodejs/index.js#L1553-L1557][Haskell]], and of-course [[https://github.com/alhassy/easy-extensibility/blob/65572a283e4864d9bef157b438c33f4e47276e3a/vscodejs/index.js#L1575-L1585][Java]].\n"
  },
  {
    "file": "vscode-is-itself-a-javascript-repl",
    "title": "💐 VSCode is itself a JavaScript REPL 🔁",
    "date": "2022-08-17 Wed",
    "image": "https://raw.githubusercontent.com/alhassy/easy-extensibility/main/graphics/repl.gif 90% 90%",
    "description": "A meta-extension for VSCode that makes VSCode into a living, breathing, JS interpreter: It can execute arbitrary JS that alters VSCode on-the-fly. A gateway into the world of Editor Crafting!",
    "tags": "repl-driven-development vscode emacs javascript",
    "url": "https://alhassy.com/vscode-is-itself-a-javascript-repl",
    "history": "https://github.com/alhassy/alhassy.github.io/commits/master/posts/vscode-is-itself-a-javascript-repl.org",
    "abstract": "\nA meta-extension for VSCode that makes VSCode into a living, breathing, JS interpreter: It can execute arbitrary JS that\nalters VSCode on-the-fly. A gateway into the world of Editor Crafting!\n\n| /(Inspired by using Emacs and Lisp!)/ |\n"
  },
  {
    "file": "TypedLisp",
    "title": "Typed Lisp, A Primer",
    "date": "2019-08-21 19:29",
    "image": "emacs-birthday-present.png",
    "description": "Exploring Lisp's fine-grained type hierarchy.",
    "tags": "types lisp program-proving emacs",
    "url": "https://alhassy.com/TypedLisp",
    "history": "https://github.com/alhassy/alhassy.github.io/commits/master/posts/TypedLisp.org",
    "abstract": "\n#+TOC: headlines 2\n\nLet's explore Lisp's fine-grained type hierarchy!\n\nWe begin with a shallow comparison to Haskell, a rapid tour of type theory,\ntry in vain to defend dynamic approaches, give a somewhat humorous account of history,\nnote that you've been bamboozled ---type's have always been there---,\nthen go into technical details of some Lisp types, and finally conclude by showing\nhow /macros permit typing/.\n\n# Lisp types are fine-grained; e.g., rather than ~int~ we may use a spefied range of numbers,\n# or a set of specfiied elements, intersections, unions, and complements of types, and\n# even arbitrary predicates!\n\nGoals for this article:\n\n1. Multiple examples of type constructions in Lisp.\n2. Comparing Lisp type systems with modern languages, such as Haskell.\n3. Show how algebraic polymorphic types like ~Pair~ and ~Maybe~ can be defined in Lisp.\n   Including heterogeneously typed lists!\n4. Convey a passion for an elegant language.\n5. Augment Lisp with functional Haskell-like type declarations ;-)\n\nUnless suggested otherwise, the phrase “Lisp” refers to\n[[https://www.gnu.org/software/emacs/manual/html_mono/cl.html#index-cl_002ddeftype-14][Common Lisp as supported by Emacs Lisp]]. As such, the resulting discussion\nis applicable to a number of Lisp dialects\n---I'm ignoring editing types such as buffers and keymaps, for now.\n"
  },
  {
    "file": "three-minute-thesis",
    "title": "Have you ever packaged anything?",
    "date": "2019-03-12 19:29",
    "image": "packages.png 250 250",
    "description": "I learned something neat, and wanted to share!",
    "tags": "packages dependent-types",
    "url": "https://alhassy.com/three-minute-thesis",
    "history": "https://github.com/alhassy/alhassy.github.io/commits/master/posts/three-minute-thesis.org",
    "abstract": "\n#+TOC: headlines 2\n\n# copied from the repo\n\nHerein I try to make my current doctoral research accessible to the average person:\nExtending dependently-typed languages to implement module system features in the core\nlanguage. It's something I can direct my family to, if they're inclined to know what it is\nI've been doing lately.\n\nThe technical matter can be seen at the associated website\n─[[https://alhassy.github.io/next-700-module-systems-proposal/][The Next 700 Module Systems]]─ which includes a poster, slides, and a demo.\n\nExcluding the abstract, this is my thesis proposal in /three minutes/ (•̀ᴗ•́)و\n"
  },
  {
    "file": "InteractiveWayToC",
    "title": "An Interactive Way To C",
    "date": "2019-01-12 19:29",
    "image": "interactive_way_to_c.png 450 450",
    "description": "Learning C program proving using Emacs --reminiscent of Coq proving with Proof General.",
    "tags": "program-proving c emacs frama-c",
    "url": "https://alhassy.com/InteractiveWayToC",
    "history": "https://github.com/alhassy/alhassy.github.io/commits/master/posts/InteractiveWayToC.org",
    "abstract": "\n#+TOC: headlines 2\n\n# copied from the repo\n\nDo you know what the above program accomplishes?\nIf you do, did you also spot a special edge case?\n\nWe aim to present an approach to program proving in C using a minimal Emacs setup\nso that one may produce literate C programs and be able to prove them correct\n--or execute them-- using a single button press; moreover the output is again in Emacs.\n\nThe goal is to learn program proving using the Frama-C tool\n--without necessarily invoking its gui-- by loading the source of this file into\nEmacs then editing, executing, & proving as you read along.\nOne provides for the formal specification of properties of C programs --e.g., using ACSL--\n which can then be verified for the implementations using tools that interpret such annotation\n--e.g., Frama-C invoked from within our Emacs setup.\n\nRead on, and perhaps you'll figure out how to solve the missing ~FixMe~ pieces 😉\n\nThe intent is for rapid editing and checking.\nIndeed, the Frama-c gui does not permit editing in the gui, so one must switch between\ntheir text editor and the gui.\n[[https://orgmode.org/worg/org-tutorials/org4beginners.html][Org mode beginning at the basics]] is a brief tutorial that covers a lot of Org and,\nfrom the get-go, covers “the absolute minimum you need to know about Emacs!”\n\nIf anything, this effort can be construed as a gateway into interactive theorem proving\nsuch as with Isabelle, Coq, or Agda.\n\nThe article /aims/ to be self-contained ---not even assuming familiarity with any C!\n\n\n#+BEGIN_QUOTE\n  The presentation and examples are largely inspired by\n\n  + Gilles Dowek's exquisite text [[https://www.springer.com/gp/book/9781848820319][Principles of Programming Languages]].\n     - It is tremendously accessible!\n\n  + Allan Blanchard's excellent tutorial\n    [[https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf][Introduction to C Program Proof using Frama-C and its WP Plugin]].\n\n  Another excellent and succinct tutorial is Virgile Prevosto's [[https://frama-c.com/download/acsl-tutorial.pdf][ACSL Mini-Tutorial]].\n  In contrast, the tutorial [[https://www.cs.umd.edu/class/spring2016/cmsc838G/frama-c/ACSL-by-Example-12.1.0.pdf][ACSL By Example]] aims to provide a variety of algorithms\n  rendered in ACSL.\n#+END_QUOTE\n\nThere are no solutions since it's too easy to give up and look at the solutions that're\nnearby. Moreover, I intend to use some of the exercises for a class I'm teaching ;-)\n"
  },
  {
    "file": "PathCat",
    "title": "Graphs are to categories as lists are to monoids",
    "date": "2018-12-24 19:29",
    "image": "PathCat.png 300 300",
    "description": "A fast-paced introduction to Category Theory based on the notion of graphs.",
    "tags": "category-theory agda types",
    "url": "https://alhassy.com/PathCat",
    "history": "https://github.com/alhassy/alhassy.github.io/commits/master/posts/PathCat.org",
    "abstract": "\n#+TOC: headlines 2\n\nNumbers are the lengths of lists which are the flattenings of trees which are\nthe spannings of graphs.\nUnlike the first three, graphs have /two/ underlying types of interest\n--the vertices and the edges-- and it is getting to grips with this complexity\nthat we attempt to tackle by considering their ‘algebraic’ counterpart: Categories.\n\n# trees are just those graphs for which arbitrary points are connected by a unique undirected path.\n\nIn our exploration of what graphs could possibly be and their relationships to lists are,\nwe shall /mechanise,/ or /implement,/ our claims since there will be many details and it is easy\nto make mistakes --moreover as a self-learning project, I'd feel more confident to make"
  },
  {
    "file": "HeytingAlgebra",
    "title": "Discovering Heyting Algebra",
    "date": "2018-11-14 19:29",
    "image": "HeytingAlgebra.png 350 350",
    "description": "How do friends communicate secretly using non-invertible operations such as minimum? An introduction to Heyting Algebra --an instance of Cartesian Closed Categories!",
    "tags": "order-theory category-theory",
    "url": "https://alhassy.com/HeytingAlgebra",
    "history": "https://github.com/alhassy/alhassy.github.io/commits/master/posts/HeytingAlgebra.org",
    "abstract": "\n#+toc: headlines 2\n\nWe attempt to motivate the structure of a Heyting Algebra\nby considering ‘inverse problems’.\n\nFor example,\n+ You have a secret number $x$ and your friend has a secret number $y$, which you've\n  communicated to each other in person.\n+ You communicate a ‘message’ to each other\n  by adding onto your secret number.\n+ Hence, if I receive a number $z$, then I can /undo/ the addition operation to find the ‘message’ $m = z - y$.\n\nWhat if we decided, for security, to change our protocol from using addition to using\nminimum. That is, we encode our message $m$ as $z = x ↓ m$. Since minimum is not\ninvertible, we decide to send our encoded messages with a ‘context’ $c$ as a pair $(z, c)$.\nFrom this pair, a unique number $m′$ can be extracted, which is not necessarily the original $m$.\nRead on, and perhaps you'll figure out which messages can be communicated 😉\n\n# For example, we wrote our message on a piece of paper and placed it on a cafe bulletin board --a context!\n\nThis exploration demonstrates that relative pseudo-complements\n+ Are admitted by the usual naturals precisely when infinity is considered a number;\n+ Are /exactly/ implication for the Booleans;\n+ /Internalises/ implication for sets;\n+ Yield /the largest complementary subgraph/ when considering subgraphs.\n# + Generalise the /deduction theorem/.\n\nIn some sense, the pseudo-complement is the “best approximate inverse” to forming meets, minima, intersections.\n\nAlong the way we develop a number of the theorems describing the relationships\nbetween different structural components of Heyting Algebras;\nmost notably the internalisation of much of its own structure.\n\nThe article aims to be self-contained, however it may be helpful to\nlook at [[https://alhassy.github.io/CatsCheatSheet/LatticesCheatSheet.pdf][this lattice cheat sheet]] (•̀ᴗ•́)و\n"
  }
]