Agdaのコードを含む記事を書いて公開できるようになりました

1. はじめに

ついに Agda のコードを含む記事を書いて公開できるようになりました！サイト上ではほとんど音沙汰なしな状態でしたが、実は1年ほど前から積極的に Agda を触っており、今となっては趣味で使うプログラミング言語はほとんど Agda になっています。

インフラも整ったところなので、これからは好きなように Agda の記事を書いていきたいと考えてます。

2. 「TojoQK の投稿」について

この「TojoQK の投稿」というサイトは最初の投稿からもう6年も経過しており、途中で静的サイトジェネレータを切り替えて最終的に Emacs Lisp を駆使して、そこそこ楽にサイトデプロイできるような独自スクリプトで無理矢理成立させているという現実があります。

このようにかなり強引なビルドシステムによってかろうじて成立しているサイトなので、これに Agda による文芸的プログラミング機能をうまく組み合わせてデプロイするのは大変でした。こういった事情により、このサイトは長い間放置されてきたわけです。

技術的負債が解決したということは全くないのですが、なんとか Agda のビルドを挟んでうまく、サイトに反映できるようになったというところです。

3. Agda の lagda 機能について

このサイトは全て Org mode で書かれているのですが、なんと Agda は拡張子を .lagda.org とすることで、 Org-mode 中にかかれた Agda コードを問題なくコンパイルできます。しかも、 polymode とうまく組み合わせることで Org-mode を使いながら、Agda の型チェックもできるという夢のような状態も作れます。

たとえば、 1 + 1 = 2 をここで Agda にチェックさせてみましょう。

  module _ where
    open import Data.Nat using (ℕ; _+_)
    open import Relation.Binary.PropositionalEquality using (_≡_; refl)

    1+1≡2 : 1 + 1 ≡ 2
    1+1≡2 = refl

無事に 1 + 1 ≡ 2 であることを証明できている。すごい！ここで refl だけ色が違っているように見えると思うのですが、この色の違いの理由は refl がコンストラクタであることを意味しています。 Agdaはコンスラクタかどうかについて構文的に区別することができないので、それがコンストラクタかどうかはAgdaコンパイラだけが知っています。このAgdaコンパイラによる色付けがセマンティックハイライティングです。 Agda のコンパイルが通らない限り、この色付けは決してできないのです。

4. 2026年に個人でブログサイトを自作する意義

私は静的サイトビルドのワークフローで自作のビルドプロセスを通した後に、 Emacs の org-publish の org-html-export-to-html を通してHTMLファイルを生成しています。

この自作ビルドプロセスがもともとあったおかげで、 agda -html --html-highlight=code のようなコマンドを用いて Agda の記事を作成して公開できるようになりました。

おそらく、既成のビルドツールのプロセスに agda --html で生成したファイルで置換するみたいな処理を挟むのは、相当に面倒くさいと思うので、こればっかりは色々自力でやっていてよかったなあと感じています。

こういった圧倒的な自由度こそが、個人サイトの醍醐味だというものです。

5. Agda、Agda-stdlibのソースファイルを部分的にホスティングする問題

agda --html で .lagda.org のファイルをビルドすると、 Agdaコード中にリンクが自動的に張られクリックすると定義を見にいけるというとても便利な機能があるのですが、自分の書いたコードだけでなく Agda や Agda-stdlib のコードへのリンクが張られてしまう問題があります。

リンクが張られる以上は一緒にホスティングしないといけないという問題があるので、ここは結構どうするか考えさせられました。おそらく、Agda チームの方々はこのあたりの法的問題についてあんまり真剣に考えていないのではないかという疑惑を正直持っているのですが、少なくともMITライセンス文言に従うためには私のサイト上でライセンス表示をする必要がありそうです。

そのため、Agda の記事の場合は「※本記事はAgdaコードを含んでいます。Agdaコード中のリンク先ファイルのライセンスについてはAgda関連ライセンスについてを参照してください」という文言とリンクを張ることで解決しました。このページには Agda と Agda-stdlib のバージョン番号を乗せていて、ビルドサーバーの Agda のバージョンと食い違ったら CI がコケるようにしています。なので、バージョンが新しくなるたびにライセンス表記を手動で更新する運用でとりあえずいこうと考えています。

また、検索エンジンの検索結果に私のサイトに載った Agda のソースコードが一覧されてしまうと悪いので、 Agda, Agda-stdlib のファイルのページについては robots の指定で noindex を付けています。

6. おわりに

ともかく、Agda のコードがかけるようになってよかったです。私の趣味のプログラミングはほぼ全て Agda になっているような状況なので、 Agda の記事が書けないのは致命的な問題でした。

この記事では 1 + 1 = 2 としかいっていないですが、今後は色々思いついたことを記事にしていこうかと思っています。