gabby

@fullmoon

Author of haskellforall.com, dhall-lang.org and @trygrace.dev, professional doggirl and endurance hunter I'm a midwife to the hidden beauty in everything she/her 🏳️‍⚧️ coworkers DNI 💖 @ember.pet

145 Following2,415 Followers3,443 Posts

Bluesky

trans

Is this your profile?Claim it and fullmoon.dirty.social is yours.Claim profile

gabby@fullmoon· 18d

I thought this was a pretty interesting take from Codeberg's announcement of their anti-LLM policy They argue that many developers using LLMs are essentially heaven-banning themselves where they don't realize they're developing for a nonexistent community

# The development team of none

Using LLMs to work with your code gives you a kick of adrenaline. You can develop at a rapid pace, build things as if you had a large team. Only that you have none. In fact, you are (often) alone, working with a statistical machine that turns energy into code.

It seems like many ‘vibe coders’ don't realize that they don't actually have a community around them. They build projects as if they had, and spend resources accordingly. We see projects having a lot of code activity, heavy CI/CD testing, frequent and large release binaries. Sometimes, it feels like the amount of supported platforms exceeds the amount of actual users.

To us, it seems ridiculous to see projects with a single developer and virtually no users consuming as much or even more resources than some of the largest community projects on Codeberg, which operate frugal with CI/CD and storage resources. We do not believe it is reasonable for Codeberg to invest our precious donation money into hosting of large ghost projects.

gabby@fullmoon· 24d

eat shit seija

Screenshot of Touhou: Lost Branch of Legend final boss fight depicting Sakuya about to kill Seija with Deflation World+

gabby@fullmoon· 24d

Diana (💗 doll) 5:08 PM

you know AI has a great reputation when it's the first suspect whenever something is fucked

gabby@fullmoon· Jul 12

the illusion of free choice

Screenshot of card selection screen from Touhou: Lost Branch of Legend depicting a card reward with three options:

Option 1: Trace On (WW): Gain RR. Choose 1 of 3 random cards to add to the hand. It has Exile and Ethereal. Those cards have a total cost of 1, 2, and 3, respectively.
Option 2: Breaking Boundaries (2W): Choose 1 of 3 completely random cards to add to the hand. It temporarily costs 0 and has Exile and Ethereal.
Option 3: Marble Phantasm (XW): Choose 1 of 3 random cards with a total cost of X+1 to add into the hand. It temporarily costs 0 and has Exile and Ethereal. Exile

gabby@fullmoon· Jul 12

eat shit seija

Screenshot of Touhou: Lost Branch of Legend final boss fight where Reimu is about to finish Seija with Fist of the Hakurei+ for 174 damage

gabby@fullmoon· Jul 9

from Peopleware:

5. Parkinson’s Law Revisited

Writing in 1954, the British author C. Northcote Parkinson introduced the notion that work expands to fill the time allocated for it, now known as Parkinson’s Law.

If you didn’t know that few managers receive any management training at all, you might think there was a school they all went to for an intensive course on Parkinson’s Law and its ramifications. Even managers that know they know nothing about management nonetheless cling to that one axiomatic truth governing people and their attitude toward work: Parkinson’s Law. It gives them the strongest possible conviction that the only way to get work done at all is to set an impossibly optimistic delivery date.

gabby@fullmoon· Jul 7

To do so, we can rewrite this function: { x ? 1 }: x … like this: r: ({ x = 1; } // r).x … and then ask the reference implementation to infer the most general type, which is this one:

>>> r: ({ x = 1; } // r).x
(present Number g = present d) => { x ? g, e } -> d

gabby@fullmoon· Jul 6

eat shit seija

Screenshot of Touhou: Lost Branch of Legend final boss depicting Marisa about to kill Seija with Phoenix Wings Rise

gabby@fullmoon· Jul 5

eat shit seija

Screenshot of Touhou: Lost Branch of Legend's final boss battle, where Marisa is about to deal the killing blow against Seija using "Luna, Silent Moonlight"

gabby@fullmoon· Jul 4

look at what Type Theorists have been demanding your Respect for all this time, with all the pages we allot them

a screenshot of a proof from a type theory paper which is very long and convoluted and has a bunch of 👉👉👉👉's

gabby@fullmoon· Jul 2

new blog post incoming and I'm pretty excited about this post

Mechanized type inference for record concatenation

The context behind this post is that I'm working on a type checker and language server for Nix and there are three features of the language which make it tricky to typecheck (which I'll dub the "three horsemen of Nix type inference"):

- computed imports (imports that depend on values in scope)

- computed record fields and field accesses

- // (the right-biased record concatenation operator) which is the subject of this post!

Here "right-biased record concatenation" means combining two records, preferring fields from the right record if they overlap. For example:

nix-repl> { x = 1; y = 2; } // { y = true; z = "hi"; }
{ x = 1; y = true; z = "hi"; }

The good news is that type inference for record concatenation is not a research problem because the algorithm was published in 1991 as "Type inference for record concatenation and multiple inheritance" by Mitchell Wand (henceforth "the Wand paper"). The bad news is that as far as I can tell no language in existence implements the type inference algorithm described in that paper, so even though it's not a research problem it's still not a solved problem.

A big reason why is that the presentation in the paper is informal and not "easy to mechanize" meaning that it doesn't translate well to code and glosses over important details. In this post I hope to fix that by by spelling out a formal algorithm equivalent to the original paper. In particular, I'll formalize the algorithm in three ways:

- a declarative natural deduction semantics
- an algorithmic semantics using constraint generation and resolution
- a reference Haskell implementation (≈400 lines of code)

This post builds upon my previous post: Record type inference for dummies. Reading that post will not necessarily prepare you for this post if you're a type theory newcomer, but it will at least help you understand the basic terminology/syntax and also appreciate why this is a challenging problem to solve.

gabby@fullmoon· Jul 1

extremely obligatory

“To say that straight men are heterosexual is only to say that they engage in sex (fucking exclusively with the other sex, i.e., women). All or almost all of that which pertains to love, most straight men reserve exclusively for other men. The people whom they admire, respect, adore, revere, honor, whom they imitate, idolize, and form profound attachments to, whom they are willing to teach and from whom they are willing to learn, and whose respect, admiration, recognition, honor, reverence and love they desire… those are, overwhelmingly, other men. In their relations with women, what passes for respect is kindness, generosity or paternalism; what passes for honor is removal to the pedestal. From women they want devotion, service and sex.

Heterosexual male culture is homoerotic; it is man-loving.”
― Marilyn Frye, The Politics of Reality: Essays in Feminist Theory

gabby@fullmoon· Jun 30

only real ones will get this

Two-panel comic

Panel 1:

Girl on right: So, are you like, gay or something?

Girl on left: What?

Girl on right: What Pride flag is that?

Panel 2:

Girl on Left (in front of Republic of San Magnolia Flag): …

gabby@fullmoon· Jun 25

was just introducing my girlfriend to malbolge

Programming in Malbolge

Malbolge was very difficult to understand when it arrived, taking two years for the first Malbolge program to appear. The author himself has never written a Malbolge program.[2] The first program was not written by a human being; it was generated by a beam search algorithm designed by Andrew Cooke and implemented in Lisp.[3]

gabby@fullmoon· Jun 22

damn i fuckin nailed this tiramisu

gabby@fullmoon· Jun 22

new blog post incoming

# Record type inference for dummies

The reason I'm writing this post is because I actually wanted to write a more advanced post on type inference for anonymous records, but then I realized that most of my readers wouldn't understand the latter post in isolation. So I figured this introductory post could teach people new to type theory the basics.

The reason I'm writing *both* posts is because I believe that good type inference for anonymous records is one of the big things holding back statically typed languages[^1]. I also think that there is a large disconnect between what experts understand is possible and what lay programmers are comfortable or familiar with:

Picture:

> XKCD #2501 "Average Familiarity" edited to read:
>
> Girl: Row polymorphism is second nature to us theorists, so it's easy to forget that the average person probably only knows the judgments for records and one or two projections.
>
> Guy: … and subtyping, of course.
>
> Girl: Of course.
>
> Caption: Even when they're trying to compensate for it, experts in anything wildly overestimate the average person's familiarity with their field.

So this post (and the next one) are going to be an exposition of where the field of type theory was at **over three decades ago**, which our industry still hasn't really caught up to, yet.

gabby@fullmoon· Jun 21

XKCD #2501 "Average Familiarity" edited to read:

Girl: Row polymorphism is second nature to us theorists, so it's easy to forget that the average person probably only knows the judgments for records and one or two projections.

Guy: … and subtyping, of course.

Girl: Of course.

Caption: Even when they're trying to compensate for it, experts in anything wildly overestimate the average person's familiarity with their field.

gabby@fullmoon· Jun 20

I don't know what she's talking about

$\dfrac { \dfrac { \dfrac { \dfrac { \displaylines { \Gamma, \hat{a} \; \hat{c}: \mathtt{Attr}, \hat{b} \; \hat{d}: \mathtt{Attrs}, r: \mathtt{\{} \; x : \hat{a}, \hat{b} \; \mathtt{\}}, s: \mathtt{\{} \; x : \hat{c}, \hat{d} \; \mathtt{\}} \vdash r \Leftarrow \mathtt{\{} \; x : \hat{a}, \hat{b} \; \mathtt{\}} \\ \Gamma, \hat{a} \; \hat{c}: \mathtt{Attr}, \hat{b} \; \hat{d}: \mathtt{Attrs}, r: \mathtt{\{} \; x : \hat{a}, \hat{b} \; \mathtt{\}}, s: \mathtt{\{} \; x : \hat{c}, \hat{d} \; \mathtt{\}} \vdash s \Leftarrow \mathtt{\{} \; x : \hat{c}, \hat{d} \; \mathtt{\}} } } { \Gamma, \hat{a} \; \hat{c}: \mathtt{Attr}, \hat{b} \; \hat{d}: \mathtt{Attrs}, r: \mathtt{\{} \; x : \hat{a}, \hat{b} \; \mathtt{\}}, s: \mathtt{\{} \; x : \hat{c}, \hat{d} \; \mathtt{\}} \vdash r \; \mathtt{//} \; s \Leftarrow \mathtt{\{} \; x : \hat{a} \; \mathtt{//} \; \hat{c}, \hat{b} \; \mathtt{//} \; \hat{d} \; \mathtt{\} } } } { \Gamma, \hat{a} \; \hat{c}: \mathtt{Attr}, \hat{b} \; \hat{d}: \mathtt{Attrs}, r: \mathtt{\{} \; x : \hat{a}, \hat{b} \; \mathtt{\}}, s: \mathtt{\{} \; x : \hat{c}, \hat{d} \; \mathtt{\}} \vdash \mathtt{(} r \; \mathtt{//} \; s \mathtt{)}.x \Rightarrow \hat{a} \; \mathtt{//} \; \hat{c} } } { \Gamma, \hat{a} : \mathtt{Attr}, \hat{b} : \mathtt{Attrs}, r: \mathtt{\{} \; x : \hat{a}, \hat{b} \; \mathtt{\}} \vdash s \mathtt{:} \; \mathtt{(} r \; \mathtt{//} \; s \mathtt{)} \mathtt{.} x \Rightarrow \forall (c : \mathtt{Attr}) \; (d : \mathtt{Attrs}) . \mathtt{\{} \; x : c, d \; \mathtt{\}} \rightarrow \hat{a} \; \mathtt{//} \; c } } { \Gamma \vdash r \mathtt{:} \; s \mathtt{:} \; \mathtt{(} r \; \mathtt{//} \; s \mathtt{)} \mathtt{.} x \Rightarrow \forall (a \; c : \mathtt{Attr}) \; (b \; d: \mathtt{Attrs}) . \mathtt{\{} \; x : a, b \; \mathtt{\}} \rightarrow \mathtt{\{} \; x : c, d \; \mathtt{\}} \rightarrow a \; \mathtt{//} \; c }$

gabby@fullmoon· Jun 19

I love how papers will start off with a little blurb like "So, yeah, type inference is a good idea. Anyway, now that we've gotten that out of the way let me explain my new type inference algorithm"

1. Introduction

A practical motivation for type inference is to ensure an operational safety property of programs that are well-typed: that is, when we execute a well-typed program, we are guaranteed that we will never get an error message such as "bad function `nil`."

Our goal is to extend this safety property to programs involving records and objects. Here the safety property is that we will never get a message such as "can't find field" when we attempt to do a field extraction operation. For object-oriented programming, we wish to guarantee that we will never get message such as "can't find method"

gabby@fullmoon· Jun 19

#autismspeaks

$$$ \begin{aligned} e \Coloneqq \quad & x \mathtt{:} \; e & \text{lambda with universal argument} \\ | \quad & \mathtt{\{} \; \overline{arg \mathtt{,}} \; \mathtt{\ldots}^? \; \mathtt{\}} \mathtt{:} \; e & \text{lambda with formal arguments} \\ | \quad & x \mathtt{@} \mathtt{\{} \; \overline{arg \mathtt{,}} \; \mathtt{\ldots}^? \; \mathtt{\}} \mathtt{:} \; e & \text{lambda with both} \\ | \quad & \mathtt{assert} \; e \mathtt{;} \; e & \text{assertion} \\ | \quad & \mathtt{with} \; e \mathtt{;} \; e & \text{with expression} \\ | \quad & \mathtt{let} \; \overline{b} \; \mathtt{in} \; e & \text{let expression} \\ | \quad & \mathtt{!} e & \text{boolean negation operator} \\ | \quad & \mathtt{-} e & \text{unary negation operator} \\ | \quad & e \; \mathtt{|>} \; e & \text{pipe operator} \\ | \quad & e \; \mathtt{==} \; e & \text{equality operator} \\ | \quad & e \; \mathtt{<} \; e & \text{less than operator} \\ | \quad & e \; \mathtt{\&\&} \; e & \text{and operator} \\ | \quad & e \; \mathtt{||} \; e & \text{or operator} \\ | \quad & e \; \mathtt{+} \; e & \text{addition operator} \\ | \quad & e \; \mathtt{-} \; e & \text{subtraction operator} \\ | \quad & e \; \mathtt{*} \; e & \text{multiplication operator} \\ | \quad & e \; \mathtt{/} \; e & \text{division operator} \\ | \quad & e \; e & \text{function application} \\ | \quad & e \mathtt{.} a \overline{\mathtt{.} a} & \text{ selection operator} \\ | \quad & e \mathtt{.} a \overline{\mathtt{.} a} \; \mathtt{or} \; e & \text{or expression} \\ | \quad & x & \text{variable} \\ | \quad & \textquotedblleft s^\star \textquotedblright & \text{string} \\ | \quad & n & \text{number} \\ | \quad & \mathtt{\sim} \overline{/ s^\star} & \text{home-anchored path} \\ | \quad & \mathtt{.} \overline{/ s^\star} & \text{relative path} \\ | \quad & / s^\star \overline{/ s^\star} & \text{absolute path} \\ | \quad & \mathtt{<} s \overline{/ s} \mathtt{>} & \text{search path} \\ | \quad & \mathtt{\{} \; \overline{b} \; \mathtt{\}} & \text{attr…$