Table of contents

Type systems

Liquid Types

• A Gentle Introduction to Liquid Types [published 2015-09-19; visited 2025-02-09T21:06:07Z]
• Liquid Types [published 2008; visited 2025-02-09T21:07:31Z]

Unification

• Unification (Eli Bendersky)
  • Article: Unification - Eli Bendersky's website [published 2018-11-12; visited 2025-09-14T14:05:04Z]
  • Hacker News: Unification (2018) | Hacker News [published 2025-08-18T07:11:00; visited 2025-09-14T15:41:54Z]
  • Papers referenced in the article:
    • Bugs:
      • Peter Norvig. Correcting a widespread error in unification algorithms. 1991. [PDF] Correcting a widespread error in unification algorithms | Semantic Scholar , which again links to
        • Peter Norvig. Correcting a widespread error in unification algorithms. Software: Practice and Experience. Volume 21, Issue 2. Pages 231-233. 1991. Correcting a widespread error in unification algorithms - Norvig - 1991 - Software: Practice and Experience - Wiley Online Library [visited 2025-09-14T20:57:21Z]
        • https://norvig.com/unify-bug.pdf [visited 2025-09-14T20:58:29Z]
    • Overview of the efficiency of unification algorithms:
      • Alberto Martelli, Ugo Montanari. An Efficient Unification Algorithm. ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 4, Issue 2. Pages 258 - 282. 1982. An Efficient Unification Algorithm | ACM Transactions on Programming Languages and Systems [visited 2025-09-14T15:55:54Z] (open access)
      • Kevin Knight. Unification: a multidisciplinary survey. ACM Computing Surveys (CSUR), Volume 21, Issue 1. Pages 93 - 124. 1989: Unification: a multidisciplinary survey | ACM Computing Surveys [visited 2025-09-14T18:36:32Z] (free access)

  • In the post Brought back memories to over a decade ago with Mathematica. It's quite easy to ... | Hacker News [published 2025-08-18T08:44:33; visited 2025-09-14T15:19:45Z] of the Hacker News discussion, one can find a simple example of pattern matching in Wolfram (Mathematica):

    expr = foo[bar[k], baz[V]]; expr /. foo[x_, baz[y_]] :> {x, y}

    which results in

    {bar[k], V}

• Don't Implement Unification by Recursion
  • Article: Don’t Implement Unification by Recursion | Hey There Buddo! [published 2024-10-28; visited 2025-09-14T01:50:05Z]
  • Hacker News: Don't implement unification by recursion | Hacker News [published 2024-10-28T17:53:21; visited 2025-09-14T01:49:25Z]

  • Book linked in the article:

    Franz Baader, Tobias Nipkow
    Term Rewriting & All That
    https://www.amazon.de/Term-Rewriting-That-Franz-Baader/dp/0521779200/ [visited 2025-09-14T01:52:35Z]

  • TODO: List references from article (and Hacker News) (lots of them)