HN Distilled

Essential insights from Hacker News discussions

Typechecker Zoo

Original Article

Hacker News Discussion

The Hacker News discussion revolves around a technical article implementing various type systems, with users offering feedback on content, presentation, and the technical details discussed. Key themes include the use and perceived quality of AI-generated art, the technical depth and scope of the implementations, and specific criticisms of the article's statements about type checking.

AI-Generated Art and Presentation

A significant portion of the discussion centers on the visual elements of the webpage, specifically the AI-generated animal pictures. The placement and relevance of these images are questioned, with some users finding them distracting and aesthetically unappealing.

  • Ambiguity and Perceived Lack of Meaning: Some users were confused by the symbols in the images, initially assuming they held technical relevance. > voidUpdate: "I'm a little confused by the cutesy animal pictures on the first page... The only one that doesnt have some kind of lambda scribbled on them is the one that is directly lambda calculus, and I can't work out what some of the other symbols are even meant to be..."

  • Ornamental, Non-Intentional Use: The consensus appears to be that the symbols are not meaningful but rather decorative elements. > webstrand: "I'm pretty sure they're AI generated art, I don't think the symbols are intentional or have any meaning. They're basically ornamental section dividers."

  • Unnecessary and Detracting: A strong sentiment is that the AI art is superfluous and detracts from the article's value. > thrance: "Unecessary AI generated slop no one asked for, that made me close the webpage. When will authors realize that unrelated ugly AI art only removes values from their articles?"

  • Critique of size: One user questioned the size of these ornamental elements. > MarkusQ: "In that case, why so big?"

  • Technical Suggestions for Readability: Beyond the art, a practical suggestion was made regarding the code block styling to improve readability, especially in dark mode environments. > verandaguy: "To the author: consider adding a dark theme to the code blocks. As-is, viewed on a system with a dark theme, these default to a _really low-contrast light theme that's hard to read even without vision issues."

Technical Content and Implementation Depth

Users also engaged with the technical aspects of the article, discussing the type systems being implemented and their theoretical underpinnings.

  • Resource for Learning: The article is recognized as a valuable resource for understanding specific type system implementations. > dunham: "This is a great resource to learn how normalization by evaluation and insertion and solving of implicit variables is implemented."

  • Scope of Implementations: There's discussion about which specific type theories are being implemented, with a comparison to established systems. > tromp: "The CoC implementation includes inductive types, so is this an implementation of CiC, the Calculus of Inductive Constructions, with the same proving power as Lean?" > cwzwarich: "Lean’s type theory extends CIC with the (global) axiom of choice, which increases consistency strength over base CIC."

  • Comparison to Other Type Checkers: Users brought up alternative or foundational type checking approaches, suggesting areas for expansion or comparison. > chubot: "This seems to jump straight into type inference and bidirectional type checking, without a basic UNI-directional type checker" > chubot: "e.g. Featherweight Java (chapter 19 of TAPL by Pierce) is expressed with a simple unidirectional algorithm" > chubot: "And some of the languages in the PL Zoo - https://plzoo.andrej.com/" > chubot: "like https://github.com/andrejbauer/plzoo/blob/master/src/sub/typ... , although I am not quite sure"

  • Proposal for Additional Implementations: A suggestion was made for implementing other influential type system variants. > choeger: "Proposal: Also implement the efficient Hindley/Milner variant used by the OCaml compiler. IIRC it is inspired by garbage collection and much faster than the original."

Critiques of Generalizations and Missing Context

A significant point of contention arose from the article's generalizations about type systems and their evolution, particularly concerning the role of functional programming and bidirectional type checking.

  • The Role of "Functional": A user argued that the article overlooked the importance of "functional" in describing modern statically typed languages. > chubot: "We’re going to create minimal implementations of the most successful static type systems of the last 50 years." > chubot: "As a result, many modern statically-typed languages have converged on a practical and elegant middle ground: bidirectional type checking." > chubot: "I think what is missing in both statements is the word FUNCTIONAL."

  • Counter-Examples to Bidirectional Type Checking: The user provided examples of modern statically typed languages that may not fit the "bidirectional" categorization and questioned whether the authors would include them. > chubot: "e.g. Go, Rust, Swift, D, and Zig are modern statically typed languages, that are not functional. And I'm not sure if the authors would consider them "bidirectional""

  • Concerns about AI Bias in Information Gathering: The user expressed skepticism about relying on LLM responses for this information, highlighting a potential for repeating "AI slop." > chubot: "I would like to see someone write about that. (I posed this query to 3 LLMs, and they mostly agree that those languages don't use bidirectional type checking; however I am wary of repeating AI slop)"

  • Support for the Critique: Another user chimed in with a specific example regarding Rust's type checking, seemingly contradicting the generalization. > Ar-Curunir: "Rust uses bidirectional type checking"

  • Connection to Philosophical/Theoretical Criticism: The discussion also drew parallels to existing critiques of certain theoretical paradigms in programming languages. > chubot: "This part also reminds me of Against Curry-Howard Mysticism - https://liamoc.net/forest/loc-000S/index.xml - https://lobste.rs/s/n0whur/against_curry_howard_mysticism" > chubot: "A deep insight has been unfolding since the late 1970s, a revelation that three immense, seemingly distinct realms of human thought are echoes of a single, deeper reality. "