関数型まつり2026
このページではwindymelt.iconが参加した関数型まつり2026の感想をまとめてある。
聞いた発表
ElixirとBEAM VMの力を生かして、堅牢なサーバを構成できる。
ラズバイを利用してプロセスマイグレーションを行うデモがあった。
センサーノードでは故障などでフェイルオーバー(F/O)しなければならないこともあるはずで、たとえばVRRPみたいな機構で受動的にF/Oもできるが、このデモのように自分の異常を検知したタイミングでプロセスを他のVMに投げることで能動的にF/Oすることもできるよなーと思った。
知ったライブラリ
Zenoh
Giocci
Zenhex
ModBuzz
質疑(windymelt.iconによる)
Q. ARMでも動く？
A. Linuxが動作する普通のプロセッサなら動く。AtomVMならESP32みたいな特殊な(弱い)環境でも動く。Nervesというミドルウェアを利用することで毎回ファームを焼くことなくTCP/IP経由でコードをアップロードできてべんり
感想
組込みで活躍しそうな言語だなーという印象だった。
Rustも組込みで活躍しそうだが、ちょっと毛色が違う。Rustは安全性とかセンサーそのものの実装で、Elixir/Erlang/BEAM VMはそれをまとめる通信系の基盤として有用な感じ。
そういえばPleromaというActivityPubの実装もElixirだった。そういうの得意だよね。 最近UUIDが流行っているのでUUID配ってくれるサーバとか作るとおもしろいかもしれない
Akka StreamライクなDSLをRustで作るとどうなるか？という発表。
Asyncの境界でいい感じにアクターの境界を作るなどして、ストリーム処理のメンタルモデルをうまくアクターシステムに落とし込んでいく。コンパイラやね。
Scalaのジェネリクス、すなわち型パラメータを利用して暗号をうまくドメイン領域に持ち上げて扱う試みの紹介。
著者はFOLIO(証券・金融企業)のエンジニア。なるほど暗号化したそうなドメインですね
したいしたくない以前に「コンプライアンスやポリシー、法令上必要」なこともある
一般に、暗号化処理はシリアライズと暗号化の2フェイズに分けられる
シリアライズ: JSONとかにしてOctet Arrayにする
暗号化: Octet Arrayを暗号アルゴリズムと鍵、必要によってIVを利用して、暗号化されたOctet Arrayにする
ところで、例えばUserを暗号化したとすると素朴にはArray[Byte]になってしまう。これだとUserを暗号化したんだよーという情報が潰れてしまう。これだと別のドメインモデルであるEmailみたいなやつと混同してしまう余地を生んでしまう
そこで、EncryptedUserみたいな型を作ると便利なのだが、EncryptedEmailとかEncryptedMessageみたいなものが大量に登場してしまう
ドメインモデルがれば、それに応じて暗号化されたモデルも増えてしまう
必要な都度モデルを定義しなければならない。「暗号化されたなにか」に対する共通処理も定義しにくい
traitを継承させるのもなんかちがう
すべてのドメインモデルに対して暗号化された型が欲しいのだから、ここで型パラメータの出番となる
Encrypted[A]型を用意する
この型の要件
A => Encrypted[A]が定義できること
Encrypted[A] => Aが定義できること
(ここでは鍵とかは無視してそう。アプリケーションの要求上、鍵は起動タイミングで一意に定まるのだろう)
ところで暗号アルゴリズム自体はStringをとる。AとStringを橋渡しする必要がある
シリアライザが必要
そこで、Encryptable[A]を用意する
A => Encryptable[A]が定義できること
! Encryptable[A] => Option[A]が定義できること 前述のEncrypted[A]よりも要求が弱い
ところで、(B => A, A => Option[B])という対をPrism[A, B]という
Prismは合成に関して色々と都合の良い振舞いをするので、Prismとして定式化すると便利
「暗号化できるものしか暗号化の対象たりえない」ので、Encrypted[A: Encryptable]と書けるようになる
感想
型クラスのとても良い題材だと思った。
題材として実務に即しており、理論的な複雑さをともなわない点
あるモデルAを暗号化したい、ということをEncrypted[A]で表現できる、という導入が自然である点
そこから、「暗号化可能である」という特定の型にまつわる性質をEncryptable[A]として表現した点
そもそもこの二者の違いとはなんなのか？という問いが自然に生まれる点
型の話だけかと思いきや、Prismが登場するのも良い。
数学的にパラメトリシティについて見ていく発表。難しかった。
F[A]みたいな型があるとき、特定のA⊃aに依存しないような実装をF[A]について考えているはず。
それは、実装がなんらかの条件で縛られ、限定されているのでは？という直感が生じる
それを数学的に確認する
PythonとかでDNNを学習させることはいまどきよくある。しかしテンソルの形が違うのは動的に検査しており、数時間走らせてからエラーでおじゃんになる、ということもある
コンパイルタイムでやりたいねん
Leanとか使うと証明を書くことで確実に形状が合致することを保証できるが、しかし証明を書きたいわけではない。ちゃんと動くことだけ知りたい
うまいこと多段階計算でやりましょう
なぜかScala界隈でも利用者が多いNix。
どういうメンタルモデルでやってるのか？という話題
暗号関連処理では定期的にデカいCVEが出ている。しかしそれらの原因としては素朴なコーディングミスがある
Heartbleedでは入力由来の(unsafeな!)整数を境界検査済みの長さとして扱ってしまったことで不変条件が破壊され、脆弱性につながった
Apple Goto failでは状態をうまく扱えなかったことで脆弱性につながった
ところでRailway Oriented Programmingというのがある
保証が増えていく型変換としてこれを見てみよう
Raw(ナマのユーザがよこした値) -> Parsed(シンタックス上有効である) -> Validated(セマンティクス？上有効である) -> Verified(より強い保証)のように
われわれには型システムがある。これをどう活用するべきか？
仕様が守るべき振舞いを、ある型のコンストラクタが作る型の不変条件へと写すことで、コードに強い保証を与える
多くのライブラリが実装されているC言語上でいくら安全性をチェックする変更を行ったところで、それは制御フロー上の局所的なチェックでしかない。そこで生じた意味的な情報は消え失せる
後続のフローにはそのような情報は載らない。
windymelt.icon 型システムでおれたちがやりたいのって、意味論的な情報を構文論的な情報へと転写する、すなわち「保証したりしたいなんらかの情報」を型へと落とし込むことなんだよなぁ
値として残らなくとも、型として残すことはできる
値が不要でも型として残したほうがいい
検証状態をうまく扱えずに脆弱性を埋め込んでしまったGoto failでも同じことがいえる
重要な情報は制御フローに埋め込むのではなく、値や型に埋めなければならない
windymelt.icon こうして具体的な疑似コードVerified<T>を見るだけでも、全称型(ジェネリクス)がもたらす表現力ってものすごく強いことがわかるなぁ（だからこそ現代的なほとんどの言語に実装されていることだなあ）（詠嘆）
状態遷移と検証結果とを1つの関数にして同時に扱う
？
libsshの脆弱性では、プロトコルの状態遷移と検証の方向を扱い間違えて脆弱性となった
ADTで状態を表現することで、そもそも間違った状態に遷移できなくする
Typestateという設計手法。到達可能な状態を型として扱うことで、そもそも間違えなくする
状態は構造体である(ADTである)
状態には遷移処理のみを実装する
状態遷移によって所有権を消費する
旧状態を利用できなくする
nonceの再利用を禁じることを、affine stateで表現する
<<なんらかの>>境界を越えたら、同じ型のままにしない
型とは集合であるという素朴な見方もある一方で、型とは境界を引くものである、という定義もできそう。
その<<なんらか>>を定義していくのがモデリング
バックエンドシステムはほぼScala。
証券システムはロジックの塊。しかもドメイン境界があり、色々なサブシステムがある
Scalaは言語ネイティブな堅牢性がある
後付けで色々保証する言語とは統合性が違う
windymelt.icon 型って大量の(ある種の承認が通ったとかKYCできたといった)「前提」を圧縮したものだよなー
Scalaは標準機能で強力な型による庇護が得られる
windymelt.icon Refinedやfs2使っているのがアツいなぁ。業務ルールといったビジネス的な複雑さと、リソース解放の保証といったテクニカルな複雑さを同時に型で保証している
副作用を正しく型で表現する
トランザクション境界を見極める
分散トランザクションを避ける
綺麗に書けることを強制しない
Scala未経験者でも採用して持続可能にやる
関数型言語としてのScalaを利用できる人材を育てるというよりは、堅牢なシステムを構築するための技術や考え方を学び、その延長線上に当然Scalaがいる、という感じ
Scalaは本質的に自由な言語である。チームで細やかな舗装をする
感想
Scalaでぜんぜんやっていけますよ、という自信が得られたよい発表だった。
Scalaは良い言語なんだけど採用がね・・・みたいな話にすぐなるのだが、そんなに複雑な言語でもないので、採用してからキャッチアップしてもらう、でもぜんぜん問題ない。
Better Javaとして学べばいい
Scalaは複雑なこともできる言語であって、最初から複雑な機能をつかいこなす必要はまったくない
Scalaのうまみは複雑なことをしなくても得られる
その他
FOLIOさんのブースでは、なんと業務コードが展示されていた。その場でintellijをいじって見せてくれる。
Scalaの現役コードが見られて嬉しかった。Scalaは業務コードとしてぜんぜん無理なく使われている。
業務事例は貴重なので、ありがたい
Scalaはバックエンドサーバの言語として実運用に耐える、という確信が強まった
はてなでもMackerelやはてなブックマークでScalaを利用している。