So, you're captivated by the fediverse—the decentralized social web powered by protocols like ActivityPub. Maybe you're dreaming of building the next great federated app, a unique space connected to Mastodon, Lemmy, Pixelfed, and more. The temptation to dive deep and implement ActivityPub yourself, from the ground up, is strong. Total control, right? Understanding every byte? Sounds cool!

But hold on a sec. Before you embark on that epic quest, let's talk reality. Implementing ActivityPub correctly isn't just one task; it's like juggling several complex standards while riding a unicycle… blindfolded. It’s hard.

That's where Fedify comes in. It's a TypeScript framework designed to handle the gnarliest parts of ActivityPub development, letting you focus on what makes your app special, not reinventing the federation wheel.

This post will break down the common headaches of DIY ActivityPub implementation and show how Fedify acts as the super-powered pain reliever, starting with the very foundation of how data is represented.

Challenge #1: Data Modeling—Speaking ActivityStreams & JSON-LD Fluently

At its core, ActivityPub relies on the ActivityStreams 2.0 vocabulary to describe actions and objects, and it uses JSON-LD as the syntax to encode this vocabulary. While powerful, this combination introduces significant complexity right from the start.

First, understanding and correctly using the vast ActivityStreams vocabulary itself is a hurdle. You need to model everything—posts (Note, Article), profiles (Person, Organization), actions (Create, Follow, Like, Announce)—using the precise terms and properties defined in the specification. Manual JSON construction is tedious and prone to errors.

Second, JSON-LD, the encoding layer, has specific rules that make direct JSON manipulation surprisingly tricky:

• Missing vs. Empty Array: In JSON-LD, a property being absent is often semantically identical to it being present with an empty array. Your application logic needs to treat these cases equally when checking for values. For example, these two Note objects mean the same thing regarding the name property:

  // No name property
  {
    "@context": "https://www.w3.org/ns/activitystreams",
    "type": "Note",
    "content": "…"
  }

  // Equivalent to:
  {
    "@context": "https://www.w3.org/ns/activitystreams",
    "type": "Note",
    "name": [],
    "content": "…"
  }

• Single Value vs. Array: Similarly, a property holding a single value directly is often equivalent to it holding a single-element array containing that value. Your code must anticipate both representations for the same meaning, like for the content property here:

  // Single value
  {
    "@context": "https://www.w3.org/ns/activitystreams",
    "type": "Note",
    "content": "Hello"
  }

  // Equivalent to:
  {
    "@context": "https://www.w3.org/ns/activitystreams",
    "type": "Note",
    "content": ["Hello"]
  }

• Object Reference vs. Embedded Object: Properties can contain either the full JSON-LD object embedded directly or just a URI string referencing that object. Your application needs to be prepared to fetch the object's data if only a URI is given (a process called dereferencing). These two Announce activities are semantically equivalent (assuming the URIs resolve correctly):

  {
    "@context": "https://www.w3.org/ns/activitystreams",
    "type": "Announce",
    // Embedded objects:
    "actor": {
      "type": "Person",
      "id": "http://sally.example.org/",
      "name": "Sally"
    },
    "object": {
      "type": "Arrive",
      "id": "https://sally.example.com/arrive",
      /* ... */
    }
  }

  // Equivalent to:
  {
    "@context":
    "https://www.w3.org/ns/activitystreams",
    "type": "Announce",
    // URI references:
    "actor": "http://sally.example.org/",
    "object": "https://sally.example.com/arrive"
  }

Attempting to manually handle all these vocabulary rules and JSON-LD variations consistently across your application inevitably leads to verbose, complex, and fragile code, ripe for subtle bugs that break federation.

Fedify tackles this entire data modeling challenge with its comprehensive, type-safe Activity Vocabulary API. It provides TypeScript classes for ActivityStreams types and common extensions, giving you autocompletion and compile-time safety. Crucially, these classes internally manage all the tricky JSON-LD nuances. Fedify's property accessors present a consistent interface—non-functional properties (like tags) always return arrays, functional properties (like content) always return single values or null. It handles object references versus embedded objects seamlessly through dereferencing accessors (like activity.getActor()) which automatically fetch remote objects via URI when needed—a feature known as property hydration. With Fedify, you work with a clean, predictable TypeScript API, letting the framework handle the messy details of AS vocabulary and JSON-LD encoding.

Challenge #2: Discovery & Identity—Finding Your Actors

Once you can model data, you need to make your actors discoverable. This primarily involves the WebFinger protocol (RFC 7033). You'd need to build a server endpoint at /.well-known/webfinger capable of parsing resource queries (like acct: URIs), validating the requested domain against your server, and responding with a precisely formatted JSON Resource Descriptor (JRD). This JRD must include specific links, like a self link pointing to the actor's ActivityPub ID using the correct media type. Getting any part of this wrong can make your actors invisible.

Fedify simplifies this significantly. It automatically handles WebFinger requests based on the actor information you provide through its setActorDispatcher() method. Fedify generates the correct JRD response. If you need more advanced control, like mapping user-facing handles to internal identifiers, you can easily register mapHandle() or mapAlias() callbacks. You focus on defining your actors; Fedify handles making them discoverable.

// Example: Define how to find actors
federation.setActorDispatcher(
  "/users/{username}",
  async (ctx, username) => { /* ... */ }
);
// Now GET /.well-known/webfinger?resource=acct:username@your.domain just works!

Challenge #3: Core ActivityPub Mechanics—Handling Requests and Collections

Serving actor profiles requires careful content negotiation. A request for an actor's ID needs JSON-LD for machine clients (Accept: application/activity+json) but HTML for browsers (Accept: text/html). Handling incoming activities at the inbox endpoint involves validating POST requests, verifying cryptographic signatures, parsing the payload, preventing duplicates (idempotency), and routing based on activity type. Implementing collections (outbox, followers, etc.) with correct pagination adds another layer.

Fedify streamlines all of this. Its core request handler (via Federation.fetch() or framework adapters like @fedify/express) manages content negotiation. You define actors with setActorDispatcher() and web pages with your framework (Hono, Express, SvelteKit, etc.)—Fedify routes appropriately. For the inbox, setInboxListeners() lets you define handlers per activity type (e.g., .on(Follow, ...)), while Fedify automatically handles validation, signature verification, parsing, and idempotency checks using its KV Store. Collection implementation is simplified via dispatchers (e.g., setFollowersDispatcher()); you provide logic to fetch a page of data, and Fedify constructs the correct Collection or CollectionPage with pagination.

// Define inbox handlers
federation.setInboxListeners("/inbox", "/users/{handle}/inbox")
  .on(Follow, async (ctx, follow) => { /* Handle follow */ })
  .on(Undo, async (ctx, undo) => { /* Handle undo */ });

// Define followers collection logic
federation.setFollowersDispatcher(
  "/users/{handle}/followers",
  async (ctx, handle, cursor) => { /* ... */ }
);

Challenge #4: Reliable Delivery & Asynchronous Processing—Sending Activities Robustly

Sending an activity requires more than a simple POST. Networks fail, servers go down. You need robust failure handling and retry logic (ideally with backoff). Processing incoming activities synchronously can block your server. Efficiently broadcasting to many followers (fan-out) requires background processing and using shared inboxes where possible.

Fedify addresses reliability and scalability using its MessageQueue abstraction. When configured (highly recommended), Context.sendActivity() enqueues delivery tasks. Background workers handle sending with automatic retries based on configurable policies (like outboxRetryPolicy). Fedify supports various queue backends (Deno KV, Redis, PostgreSQL, AMQP). For high-traffic fan-out, Fedify uses an optimized two-stage mechanism to distribute the load efficiently.

// Configure Fedify with a persistent queue (e.g., Deno KV)
const federation = createFederation({
  queue: new DenoKvMessageQueue(/* ... */),
  // ...
});
// Sending is now reliable and non-blocking
await ctx.sendActivity({ handle: "myUser" }, recipient, someActivity);

Challenge #5: Security—Avoiding Common Pitfalls

Securing an ActivityPub server is critical. You need to implement HTTP Signatures (draft-cavage-http-signatures-12) for server-to-server authentication—a complex process. You might also need Linked Data Signatures (LDS) or Object Integrity Proofs (OIP) based on FEP-8b32 for data integrity and compatibility. Managing cryptographic keys securely is essential. Lastly, fetching remote resources risks Server-Side Request Forgery (SSRF) if not validated properly.

Fedify is designed with security in mind. It automatically handles the creation and verification of HTTP Signatures, LDS, and OIP, provided you supply keys via setKeyPairsDispatcher(). It includes key management utilities. Crucially, Fedify's default document loader includes built-in SSRF protection, blocking requests to private IPs unless explicitly allowed.

Challenge #6: Interoperability & Maintenance—Playing Nicely with Others

The fediverse is diverse. Different servers have quirks. Ensuring compatibility requires testing and adaptation. Standards evolve with new Federation Enhancement Proposals (FEPs). You also need protocols like NodeInfo to advertise server capabilities.

Fedify aims for broad interoperability and is actively maintained. It includes features like ActivityTransformers to smooth over implementation differences. NodeInfo support is built-in via setNodeInfoDispatcher().

Challenge #7: Developer Experience—Actually Building Your App

Beyond the protocol, building any server involves setup, testing, and debugging. With federation, debugging becomes harder—was the message malformed? Was the signature wrong? Is the remote server down? Is it a compatibility quirk? Good tooling is essential.

Fedify enhances the developer experience significantly. Being built with TypeScript, it offers excellent type safety and editor auto-completion. The fedify CLI is a powerful companion designed to streamline common development tasks.

You can quickly scaffold a new project tailored to your chosen runtime and web framework using fedify init.

For debugging interactions and verifying data, fedify lookup is invaluable. It lets you inspect how any remote actor or object appears from the outside by performing WebFinger discovery and fetching the object's data. Fedify then displays the parsed object structure and properties directly in your terminal. For example, running:

$ fedify lookup @fedify-example@fedify-blog.deno.dev

Will first show progress messages and then output the structured representation of the actor, similar to this:

// Output of fedify lookup command (shows parsed object structure)
Person {
  id: URL "https://fedify-blog.deno.dev/users/fedify-example",
  name: "Fedify Example Blog",
  published: 2024-03-03T13:18:11.857Z, // Simplified timestamp
  summary: "This blog is powered by Fedify, a fediverse server framework.",
  url: URL "https://fedify-blog.deno.dev/",
  preferredUsername: "fedify-example",
  publicKey: CryptographicKey {
    id: URL "https://fedify-blog.deno.dev/users/fedify-example#main-key",
    owner: URL "https://fedify-blog.deno.dev/users/fedify-example",
    publicKey: CryptoKey { /* ... CryptoKey details ... */ }
  },
  // ... other properties like inbox, outbox, followers, endpoints ...
}

This allows you to easily check how data is structured or troubleshoot why an interaction might be failing by seeing the actual properties Fedify parsed.

Testing outgoing activities from your application during development is made much easier with fedify inbox. Running the command starts a temporary local server that acts as a publicly accessible inbox, displaying key information about the temporary actor it creates for receiving messages:

$ fedify inbox
✔ The ephemeral ActivityPub server is up and running: https://<unique_id>.lhr.life/
✔ Sent follow request to @<some_test_account>@activitypub.academy.
╭───────────────┬─────────────────────────────────────────╮
│ Actor handle: │ i@<unique_id>.lhr.life                  │
├───────────────┼─────────────────────────────────────────┤
│   Actor URI:  │ https://<unique_id>.lhr.life/i          │
├───────────────┼─────────────────────────────────────────┤
│  Actor inbox: │ https://<unique_id>.lhr.life/i/inbox    │
├───────────────┼─────────────────────────────────────────┤
│ Shared inbox: │ https://<unique_id>.lhr.life/inbox      │
╰───────────────┴─────────────────────────────────────────╯

Web interface available at: http://localhost:8000/

You then configure your developing application to send an activity to the Actor inbox or Shared inbox URI provided. When an activity arrives, fedify inbox only prints a summary table to your console indicating that a request was received:

╭────────────────┬─────────────────────────────────────╮
│     Request #: │ 2                                   │
├────────────────┼─────────────────────────────────────┤
│ Activity type: │ Follow                              │
├────────────────┼─────────────────────────────────────┤
│  HTTP request: │ POST /i/inbox                       │
├────────────────┼─────────────────────────────────────┤
│ HTTP response: │ 202                                 │
├────────────────┼─────────────────────────────────────┤
│       Details  │ https://<unique_id>.lhr.life/r/2    │
╰────────────────┴─────────────────────────────────────╯

Crucially, the detailed information about the received request—including the full headers (like Signature), the request body (the Activity JSON), and the signature verification status—is only available in the web interface provided by fedify inbox. This web UI allows you to thoroughly inspect incoming activities during development.

When you need to test interactions with the live fediverse from your local machine beyond just sending, fedify tunnel can securely expose your entire local development server temporarily. This suite of tools significantly eases the process of building and debugging federated applications.

Conclusion: Build Features, Not Plumbing

Implementing the ActivityPub suite of protocols from scratch is an incredibly complex and time-consuming undertaking. It involves deep dives into multiple technical specifications, cryptographic signing, security hardening, and navigating the nuances of a diverse ecosystem. While educational, it dramatically slows down the process of building the actual, unique features of your federated application.

Fedify offers a well-architected, secure, and type-safe foundation, handling the intricacies of federation for you—data modeling, discovery, core mechanics, delivery, security, and interoperability. It lets you focus on your application's unique value and user experience. Stop wrestling with low-level protocol details and start building your vision for the fediverse faster and more reliably. Give Fedify a try!

Getting started is straightforward. First, install the Fedify CLI using your preferred method. Once installed, create a new project template by running fedify init your-project-name.

Check out the Fedify tutorials and Fedify manual to learn more. Happy federating!

지적 재산권에 대해서 이야기를 하려면 지적 재산권 제도를 통해서 이룩하려는 것이 무엇인지를 이야기해야 합니다. 저는 지적 재산권을 세 가지로 보는데, 기능을 실현하는 것에 관련된 것과(특허, 실용신안) 표현에 관한 것과(저작권) 공정한 시장을 위한 것(상표)으로 나눌 수 있을 것 같습니다. 상표는 조금 성격이 다르다고 생각해 따로 이야기하겠지만, 어쨌든 지적 재산권이란 어떤 이로운 것을 새롭게 생각해낸 주체의 권리를 보장해주기 위한 제도지요.

그런데 이 '생각해낼 수 있는 어떤 이로운 것'이란, 대다수가 저렴하게 복제가 되거나 복제된다고 해서 그 가치가 줄어들지 않는다는 특징이 있습니다. 기능을 실현하는 지식도, 표현된 이야기도, 가끔은 '이 로고가 붙은 제품은 좋다'는 믿음도 말이지요. 어떤 면에서 말하자면, '생각해낼 수 있는 이로운 것'이 제한없이 복제될 수 있는 상태가 편익의 합을 극대화할 수도 있을 것입니다.

하지만 이렇다면, 어떠한 노력을 들여서 복제될 수 있는 무언가를 만들어내는 행위가 경제적으로 보답받지 못하는 상태가 되리라고 생각할 수 있겠지요. 우리는 그런 행위가- 발명과 창작이 사회의 편익을 증가시킨다고 이해하고 있고, 그걸 위한 인센티브를 주고 싶다고 생각합니다. 지적 재산권은 제 생각에 그것을 보장하기 위한 도구입니다. 그러나 극단적인 경우를 생각해 봅시다. 지적 재산권이 개인에게 기한과 범위 없이 인정되고, 그것을 계속 물려줄 수 있는 거지요. 불을 쓰기 위해서 처음 불을 발견한 사람의 자손에게 사용료를 내고요. 누군가가 벽에 커다란 낙서를 해서 그것을 방송으로 보도하면, 그 낙서를 복제한 것이기 때문에 보도하기 위해서 저작권료를 지불해야 할 수도 있지요. 뭐, 그러면 안 되는 건 아닐 순 있지만, 사회의 편익이 그렇게 높을 것 같지는 않습니다.

제 주장은, 지적 재산권은 다음 두 상황의 균형을 맞추는 제도라는 것입니다.

1. 지식과 표현이 아무 제한 없이 복제되어 지식과 표현을 만들어려내는 시도가 저해되거나, 사회가 원하는 만큼 이루어지지 않는 상황
2. 지식과 표현의 복제가 너무 제한되어 사회가 복제로 얻을 수 있는 편익이 감소하는 상황

대부분의 경우는 1번 상황이 문제가 됩니다. 2번 상황은 꽤 이론적인 것처럼 보이지만, 충분히 주의해서 관찰한다면 사회의 어떤 문제는 2번 상황에 해당한다는 걸 찾아보실 수도 있을 것입니다. 이미 우리의 지적 재산권은 만료, 공정 이용과 같은 방식으로 동의 없는 복제를 허용하고― 다시 말해 제작자의 권리를 무한정 인정하고 있지는 않습니다.

두 상황의 균형은 사회의 영향을 받기 때문에, 지적 재산권이 어디까지는 제작자의 권리를 보호하고 어디부터는 보호 없는 복제를 허용하게 두어야 하는지는 그 사회의 변화에 맞추어 적절하게 갱신되어야 한다고 생각합니다.

같은 것과 같지 않은 것

국밥 두 그릇의 가격이 얼마인가? KTX의 속력이 몇 km/h인가? 내일 기온은 몇 도인가? 일상에서 묻는 이런 질문은 항상 같음의 개념을 암시적으로 사용하고 있다. 앞의 예시를 보다 명시적으로 바꾼다면 아래와 같이 (다소 어색하게) 말할 수 있다.

• 국밥 두 그릇의 가격은 몇 원과 같은가?
• KTX의 속력은 몇 km/h와 같은가?
• 내일 기온은 몇 도와 같은가?

이런 질문들의 추상화인 이론들은 자연스럽게 언제 무엇과 무엇이 같은지에 대해서 답하는 데에 초점을 맞추게 된다. 예를 들면

• x2+x+1=0x^2 + x + 1 = 0의 실수 해의 갯수는 0과 같다.
• 물 분자 내의 수소-산소 연결 사이의 각도는 104.5도와 같다.
• 합병 정렬의 시간 복잡도는 O(nlog⁡n)O(n\log{n})과 같다.

등이 있다. 이렇게 어떤 두 대상이 같은지에 대해서 이야기를 하다보면 반대로 어떤 두 대상이 같지 않은지에 대해서도 이야기하게 된다. 즉,

• x+4x + 4를 22로 나눈 나머지는 x+1x + 1을 22로 나눈 나머지와 같지 않다.
• 연결 리스트(Linked List)와 배열(Array)은 같지 않다.
• 함수 λ x→x\lambda\ x \to x와 정수 55는 같지 않다.

같은 것과 판정 문제(Decision Problem)

이제 컴퓨터 과학(Computer Science)과 프로그래밍(Programming)에 있어 자연스러운 의문은 "두 대상이 같은지 아닌지와 같은 답을 주는 알고리즘(Algorithm)이 있나?"일 것이다. 다시 말해서 두 대상 aa와 bb를 입력으로 주었을 때

• 알고리즘이 참 값(True\mathtt{True})을 준다면 aa와 bb가 같고
• 알고리즘이 거짓 값(False\mathtt{False})을 준다면 aa와 bb가 같지 않은

알고리즘이 있는지 물어볼 수 있다. 이런 어떤 명제가 참인지 거짓인지 판정하는 알고리즘의 존재 여부에 대한 질문을 "판정 문제"("Decision Problem")라고 하며, 명제 PP에 대한 판정 문제에서 설명하는 알고리즘이 존재한다면 "PP는 판정 가능하다"("PP is decidable")고 한다. 즉, 앞의 질문은 "임의의 aa와 bb에 대해 aa와 bb가 같은지 판정 가능한가?"라는 질문과 같은 의미라고 할 수 있다.

이 질문에 대한 대답은 당연하게도 어떤 대상을 어떻게 비교하는지에 따라 달라진다. 예를 들어 우리가 32 비트(bit) 정수에 대해서만 이야기하고 있다면 "임의의 32 비트 정수 aa와 bb에 대해 aa와 bb가 각 비트별로 같은지 판정 가능한가?"라는 질문에 대한 답은 "그렇다"이다. 반면 우리가 비슷한 질문을 자연수를 받아 자연수를 내놓는 임의의 함수에 대해 던진다면 답은 "아니다"가 된다.^[1]

그렇다면 어떤 대상의 어떤 비교에 대해 판정 문제를 물어보아야할까? 프로그래머(Programmer)로서 명백한 대답은 두 프로그램(Program)이 실행 결과에 있어서 같은지 보는 것일 것이다. 그러나 앞서 자연수를 받아 자연수를 내놓는 함수에 대해 말했던 것과 비슷하게 두 프로그램의 실행 결과를 완벽하게 비교하는 알고리즘은 존재하지않는다. 이는 우리가 두 프로그램의 같음을 판정하고 싶다면 그 같음을 비교하는 방법에 제약을 두어야 함을 말한다. 여기서는 다음의 두 제약을 대표로 설명할 것이다.

1. 문법적 비교(Syntactic Comparison)
2. β\beta 동등성 (β\beta Equivalence)

1. 문법적 비교(Syntactic Comparison)

이 방법은 말 그대로 두 프로그램이 문법 수준에서 같은지를 보는 것이다. 예를 들어 다음의 두 JavaScript 프로그램은 문법적으로 같은 프로그램이다.

// 1번 프로그램
let x = 5;
console.log(x);

// 2번 프로그램
let x  =  5;
console.log( x );

공백문자의 사용에서 차이가 있으나, 그 외의 문법 요소는 모두 동일함에 유의하자. 반면 다음의 두 JavaScript 프로그램은 동일한 행동을 하지만 문법적으로는 다른 프로그램이다.

// 1번 프로그램
let x = 5;
console.log(x);

// 2번 프로그램
let x = 3 + 2;
console.log(x);

두 프로그램 모두 x에 5라는 값을 할당하고 5를 콘솔에 출력하나, 첫번째 프로그램은 = 5;를, 두번째 프로그램은 = 3 + 2을 사용하여 5를 할당하고 있기 때문에 문법적으로 다르다.

문법적 비교는 이렇게 문법만 보고서 쉽게 판정할 수 있다는 장점이 있으나, 두번째 예시처럼 쉽게 같은 행동을 함을 이해할 수 있는 프로그램에 대해서도 "같지 않음"이라는 결과를 준다는 단점을 가진다. 혹자는

3 + 2같은 계산은 그냥 한 다음에 비교하면 안돼? 컴파일러(Compiler)도 상수 전파(Constant Propagation) 최적화라던지로 3 + 2를 5로 바꾸잖아?

라는 생각을 할 수도 있을 것이다. 이 제안을 반영한 방법이 바로 β\beta 동등성이다.

2. β\beta 동등성

바로 앞의 소절에서 단순 계산의 추가에 의해 같음이 같지 않음으로 변하는 것을 보았다. 이런 상황을 피하기 위해서는 같음을 평가할 때 프로그램의 실행을 고려하도록 만들어야 한다. 가장 대표적인, 대부분의 프로그래밍 언어(Programming Language)에 존재하는 프로그램의 실행은 함수 호출이다. 따라서 함수 호출을 고려한 같음의 비교는 f(c)와 함수 f의 몸체 b 안에서 인자 x를 c로 치환한 것을 같다고 취급해야한다. 예를 들어

let f = (x) => x + 3;

이 있다면, f(5)와 5 + 3 혹은 8을 같은 프로그램으로 취급해야한다. 이 비교 방법의 큰 문제는 함수가 종료하는지 알지 못한다는 것이다. 두 프로그램 a와 b를 비교하는데, a가 종료하지 않는 함수 l을 호출한다면, 이 알고리즘은 "같음"이나 "같지 않음"이라는 결과를 낼 수조차 없다. 즉, 올바른 판정법이 될 수 없다.

더 심각한 문제는 아직 값을 모르는 변수가 있는 "열린 프로그램"("Open Program")에 대해서도 이런 계산을 고려해야한다는 것이다. 다음의 JavaScript 예시를 보자.

let g = (x) => f(x) + 3;
let h = (x) => (x + 3) + 3;

g와 h는 같은 프로그램일까? 우리가 g와 h가 같은 프로그램이기를 원한다면 f(x)와 x + 3을 같은 프로그램으로 보아야한다. 대부분의 프로그램은 함수 안에서 쓰여지기 때문에 프로그램의 비교는 거의 항상 g와 h의 몸체와 같은 열린 프로그램들의 비교이다. 따라서 g와 h를 다른 프로그램으로 본다면 계산을 실행하여 두 프로그램을 비교하는 의미가 퇴색되고 만다. 그렇기 때문에 우리는 x와 같이 값이 정해지지 않은 변수가 있을 때에도 f(x)을 호출하여 비교해야만 한다. 이는 우리가 단순히 모든 함수가 종료하는지 여부를 떠나서, 함수의 몸체에 등장하는 모든 부속 프로그램(Sub-program)이 종료하는지 아닌지를 따져야만 한다는 이야기이다.

이런 강한 제약조건으로 인해 β\beta 동등성을 통해서 프로그램 비교의 판정 문제를 해결 가능한 곳은 매우 제한적이지만, β\beta 동등성이 매우 유용한 한가지 경우가 있다. 바로 의존 형이론(Dependent Type Theory)의 형검사(Type Checking)이다.

의존 형이론과 형의 같음

의존 형이론은 형(Type)에 임의의 프로그램을 포함할 수 있도록 하는 형이론(Type Theory)의 한 종류이다. 예를 들어 명시적인 길이(n)를 포함한 벡터(Vector) 형을 Vector n Int과 같이 쓸 수 있다. 이 형은 n개의 Int값을 가진 벡터를 표현하는 형이다. 이제 append라는 두 벡터를 하나로 연결하는 함수를 만든다고 해보자. 대략 다음과 같은 형을 쓸 수 있을 것이다.

append : Vector n a -> Vector m a -> Vector (n + m) a

즉, append는 길이 n짜리 a 형의 벡터와 길이 m짜리 a 형의 벡터를 합쳐서 길이 n + m짜리 a 형의 벡터를 만드는 함수이다. 이 함수를 사용해서 길이 5의 벡터를 길이 2와 길이 3짜리 벡터 x, y로부터 만들고 싶다고 하자.

append x y : Vector (2 + 3) a

안타깝게도 우리는 길이 2 + 3짜리 벡터를 얻었지, 길이 5짜리 벡터를 얻진 못했다. 여기서 앞서의 질문이 다시 돌아온다.

아니, 2 + 3를 5로 계산하면 되잖아?"

그렇다. 이런 의존 형에 β\beta 동등성을 적용하면 우리가 원하는 형을 바로 얻어낼 수 있다. Vector (2 + 3) a과 Vector 5 a는 같은 형이기 때문이다. 더욱이, 의존 형의 경우 종료하지 않는 부속 프로그램이 잘못된 형을 줄 수 있기 때문에 많은 경우 종료하지 않는 부속 프로그램을 어차피 포함하지 않는다. 다시 말해, 앞서 말한 제약 조건 즉 모든 부속 프로그램이 종료해야만 한다는 제약조건은 의존 형의 경우 상대적으로 훨씬 덜 심각한 제약조건이 되는 것이다.

이런 의존 형에 있어서의 β\beta 동등성 검사를 "변환 검사"("Conversion Check")라고 하며, 두 형이 β\beta 동등일 경우 이 두 형이 서로 "변환 가능하다"("Convertible")라고 한다. 이 변환 검사는 의존 형이론 구현에 있어서 가장 핵심인 기능 중 하나이며, 가장 잦은 버그를 부르는 기능 중 하나이기도 하다.

마치며

이 글에서는 같음과 같지 않음의 판정 문제에 대해 간략히 설명하고 프로그램의 같음을 판정하는 법에 대해서 단순화하여 다루어보았다. 구체적으로는 문법 기반의 비교와 β\beta 동등성을 통한 비교로 프로그램의 같음을 판정하는 법을 알아보았고, 이 중 β\beta 동등성이 적용되는 가장 중요한 예시인 의존 형이론을 β\beta 동등성을 중점으로 짤막하게 설명하였다. 마지막 문단에서 언급했듯 의존 형이론의 구현에 있어서 β\beta 동등성을 올바르게 구현하는 것은 가장 중요한 작업 중 하나이기에, 최근 연구들은 β\beta 동등성의 구현 자체를 의존 형이론 안에서 함으로서 검증된 β\beta 동등성의 구현을 하기 시작하고 있다. 이 글이 같음과 같지 않음과 판정 문제 그리고 β\beta 동등성에 있어 유용한 설명을 내놓았기를 바라며 이만 줄이도록 하겠다.

NixOS.kr 디스코드에 올렸는데, 다른 분들의 의견을 들어보려고 해커스펍에도 올립니다. 닉스 경험이 많지 않은 사람의 글이니, 정확하지 않을 수 있습니다. 틀린 곳이 있으면 바로 알려주세요.

※ 닉스를 처음 접하는 분들이나, 닉스로 실용적인 업무를 하시는데 문제가 없는 분들한테는 적당한 글은 아닙니다. 서두에 읽으면 도움이 될만한 분들을 추려서 알려 드리려고 하니, 의외로 필요한 분들이 없겠습니다. 실무자들은 이렇게까지 파고들며 알 필요 없고, 닉스 개발자들이야 당연히 아는 내용일테고, 입문자 분들도 역시 이런 내용으로 어렵다는 인식을 갖고 시작할 필요는 없으니까요. 그럼 남은 건 하나네요. mkDerivation 동작을 이미 아는 분들의 킬링 타임용이 되겠습니다.

외국어를 익힐 때, 문법없이 실전과 부딪히며 배우는 방법이 더 좋기는 한데, 가끔은 문법을 따로 보기 전엔 넘기 힘든 것들이 있습니다. 닉스란 외국어를 익히는데도 실제 설정 파일을 많이 보는 것이 우선이지만, 가끔 "문법"을 짚고 넘어가면 도움이 되는 것들이 있습니다.

닉스 알약 (제목이 재밌네요. 알약) 글을 보면 mkDerivation이 속성 집합을 받아, 거기에 stdenv 등 기본적인 것을 추가한 속성 집합을 만들어 derivaition 함수에 넘기는 간단한 래핑 함수임을 직관적으로 잘 설명하고 있습니다.

그런데, 실제 사용 예시들을 만나면, mkDerivation에 속성 집합을 넘기지 않고, attr: {...} 형태의 함수를 넘기는 경우를 더 자주 만납니다. 그래서, 왜 그러는지 실제 구현 코드를 보고 이유를 찾아 봤습니다.

  mkDerivation =
    fnOrAttrs:
    if builtins.isFunction fnOrAttrs then
      makeDerivationExtensible fnOrAttrs
    else
      makeDerivationExtensibleConst fnOrAttrs;

mkDerivation의 정의를 보면 인자로 함수를 받았느냐 아니냐에 따른 동작을 분기합니다. 단순히, stdenv에서 가져온 속성들을 추가한다면, 함수를 인자로 받지 않아도 속성 집합을 병합해주는 //의 동작만 있어도 충분합니다.

{ a = 1; } // { b = stdenv.XXX; }

하지만, 함수로 받는 이유를 찾으면, 코드가 단순하지 않습니다. 아래는 함수를 받을 때 동작하는 실제 구현 일부를 가져 왔습니다.

makeDerivationExtensible =
    rattrs:
    let
      args = rattrs (args // { inherit finalPackage overrideAttrs; });
      ...

전체를 보기 전에 일단 args에서부터 머리가 좀 복잡해집니다. args가 args를 재귀 참조하고 있습니다. 보통 rattrs 매개 변수로는 아래와 같은 함수들이 들어 옵니다.

stdenv.mkDerivation (finalAttrs: {
  pname = "timed";
  version = "3.6.23";
  ...
    tag = finalAttrs.version;
}

(와, 해커스펍은 코드 블록에 ANSI가 먹습니다! 지원하는 곳들이 드문데요.)
코드를 바로 분석하기 전에, 닉스의 재귀 동작을 먼저 보면 좋습니다.

재귀 생각 스트레칭

nix-repl> let r = {a = 1; b = a;}; in r
error: undefined variable 'a'

위 동작은 오류지만, 아래처럼 rec를 넣어주면 가능합니다.

nix-repl> let r = rec {a = 1; b = a;}; in r 
{ a = 1; b = 1; }

※ rec동작은 Lazy 언어의 fix로 재귀를 구현하는 동작입니다. ※ 참고 Fix 함수

rec를 써서 속성 안에 정의 중인 속성에 접근할 수 있습니다. 그런데, 아래 같이 속성을 r.a 로 접근하면, rec 없이도 가능해집니다.

nix-repl> let r = {a = 1; b = r.a;}; in r
{ a = 1; b = 1; }

닉스 언어의 Lazy한 특성 때문에 가능합니다.

이제, 원래 문제와 비슷한 모양으로 넘어가 보겠습니다. 아래같은 형태로 바로 자기 자신에 재귀적으로 접근하면 무한 재귀 에러가 나지만,

nix-repl> let x = x + 1; in x
       error: infinite recursion encountered

아래처럼 람다 함수에 인자로 넘기면 얘기가 달라집니다.

nix-repl> let args = (attr: {c = 1; b = attr.a + attr.c + 1;}) (args // { a = 1; }); in args
{ b = 3; c = 1; }

여기서 속성b의 정의 동작이 중요합니다.

attr: 
  { c = 1; 
    b = attr.a + attr.c + 1;
  }

속성 b는 아직 알 수 없는, 미래의 attr에 있는 a를 받아 써먹고, 원래는 rec없이 접근하지 못했던, c에도 attr.c로 접근이 가능합니다.

원래 문제로 다시 설명하면, mkDerivation에 넘기고 있는, 사용자 함수 finalAttrs: { ... }에서, 닉스 시스템이 넣어주는 stdenv 값 같은 것들과 사용자 함수내의 속성들을 섞어서 속성 정의를 할 수 있다는 얘기입니다. 아래처럼 말입니다.

    tag = finalAttrs.version;

뭐하러, 이런 복잡한 개념을 쓰는가 하면, 단순히 속성 추가가 아니라, 기존 속성이 앞으로 추가 될 속성을 기반으로 정의되어야 할 때는 이렇게 해야만 합니다. 함수형 언어에선 자주 보이는, 미래값을 가져다 쓰는 재귀 패턴인데, 저는 아직 그리 익숙하진 않습니다.