🐥

Heftiaエフェクトシステムライブラリ入門 Part 1 - 一階エフェクト

2024/09/01に公開

Haskell

はじめに

本シリーズでは、HaskellのエフェクトシステムライブラリであるHeftiaの解説を、ライブラリ作者である筆者より行います。読者はある程度Haskellを書いたことがあるものと想定します。

本記事では、同じHaskellのエフェクトシステムライブラリであるPolysemyライブラリの説明に使用されているTeletypeエフェクト型を例として、Heftiaにおける一階のエフェクトの使い方を説明します。基本的にHeftiaは一階のエフェクトに関してはFreer Effectsと呼ばれる方式そのものであり、一階のエフェクトのみをサポートしているfreer-simple系のライブラリとあまり変わりません。そのため、Extensible Effectsを既に使ったことがある読者は、Part 1 では既存のライブラリとの違い（特に高階エフェクトと一階エフェクトのリストが分かれている点）を把握するつもりで読むと良いでしょう。Part 2 からは、既存のライブラリとはかなり使い方の異なる高階エフェクトについて説明します。

以降、常体で解説を行います。

準備

まず、Heftiaをインストールしよう。

Dockerを使ってお試し

DockerイメージでHeftiaを試すことができる^[1]。

$ git clone https://github.com/sayo-hs/heftia-docker
$ cd heftia-docker
$ docker run --rm -it -v $PWD:/work --workdir /work/example lanexpr/heftia cabal run
...
Pre-applying: Goodbye world!
Post-applying: Hello world!!
$

初期状態のコードとして、Writerエフェクトの動作例が実行される。cloneしたheftia-dockerリポジトリの中のexample/app/Main.hsを編集することで、好きなコードを試すことができる。

Dockerを使用しない通常のインストール手順

以下のインストール手順は、README.mdのInstallationを和訳したものだ。

cabalのローカルのパッケージデータベースを更新する。
```
$ cabal update
```
heftia-effects ^>= 0.3.1, ghc-typelits-knownnat ^>= 0.7 をbuild dependenciesに追加する。
必要に応じて、ghc-typelits-knownnat プラグイン、GHC2021、そして次の言語拡張を有効にする:
- LambdaCase
- DerivingStrategies
- DataKinds
- TypeFamilies
- BlockArguments
- FunctionalDependencies
- RecordWildCards
- DefaultSignatures
- PatternSynonyms
- TemplateHaskell
- PartialTypeSignatures
- AllowAmbiguousTypes

.cabalの例:

...
    build-depends:
        ...
        heftia-effects ^>= 0.3.1,
        ghc-typelits-knownnat ^>= 0.7,

    default-language: GHC2021

    default-extensions:
        ...
        LambdaCase,
        DerivingStrategies,
        DataKinds,
        TypeFamilies,
        BlockArguments,
        FunctionalDependencies,
        RecordWildCards,
        DefaultSignatures,
        PatternSynonyms,
        TemplateHaskell,
        PartialTypeSignatures,
        AllowAmbiguousTypes

    ghc-options: ... -fplugin GHC.TypeLits.KnownNat.Solver
...

このライブラリはGHC 9.2.8で動作確認をしている。
（もし動作しない例を見つけた場合、GitHubのissueにてご報告ください。）

エフェクトを定義する

まず、Teletype用のエフェクトを定義しよう。
Teletypeエフェクト型とは、仮想端末から文字列を受け取ったり、逆に表示したりするようなものだ。
ReadTTYは引数がなく、端末に入力された文字列を戻り値として返す。
WriteTTYは端末に表示する文字列を引数として取り、戻り値は空だ。

import Data.Effect.TH (makeEffectF)

-- | `Teletype`エフェクト型
data Teletype a where
    ReadTTY :: Teletype String
    WriteTTY :: String -> Teletype ()
makeEffectF [''Teletype]

makeEffectFはdata-effects-thパッケージのTemplate Haskellの関数で、これによりデータ型Teletypeを一階のエフェクト型として扱えるようになる。

具体的には、例えば以下のような関数が自動生成される。

import Control.Effect (type (<:), sendIns)

readTTY :: Teletype <: f => f String
readTTY = sendIns $ ReadTTY :: Teletype String

writeTTY :: Teletype <: f => String -> f ()
writeTTY x = sendIns $ WriteTTY x :: Teletype ()

ここでsendInsは、多相化されたエフェクトフルプログラムのキャリア（carrier. 通常はモナド）であるfへとエフェクトを送り込む関数だ。<:は、Teletypeエフェクト型のエフェクトをキャリアfへと送り込めることを表す制約だ。この自動生成により、ReadTTYエフェクトを投げたいときに毎回sendIns ReadTTYと書かなくても良くなる。

インタプリタの実装

次に、このTeletypeエフェクト型のインタプリタ（ハンドラ）を実装しよう。

import Data.Hefty.Extensible (ForallHFunctor, type (<|))
import Control.Effect (type (~>))
import Control.Effect.ExtensibleFinal (type (:!!))
import Control.Effect.Hefty (interpretRec)
import Control.Monad.IO.Class (liftIO)

-- | `Teletype`エフェクト型を、`getLine`と`putStrLn`の意味で解釈するインタプリタ。
teletypeToIO :: (IO <| r, ForallHFunctor eh) => eh :!! LTeletype ': r ~> eh :!! r
teletypeToIO = interpretRec \case
    ReadTTY -> liftIO getLine
    WriteTTY msg -> liftIO $ putStrLn msg

この関数はTeletypeのエフェクトをハンドリングするものだ。

~>、:!!、':、<|は型レベルの演算子で、(eh :!! (LTeletype ': r)) ~> (eh :!! r)というふうに結合する。

型シグネチャの~>は、その左側のエフェクト集合 (eh :!! LTeletype ': r) で表されたエフェクトフルプログラムを、右側 (eh :!! r) のものに変換するということを表している。左側に対して右側はLTeletypeが消えていることがわかる。これはつまり、Teletypeをハンドリングして、エフェクト集合から消してやるということを意味する。

interpretRecは、エフェクトのパターンマッチをする所だ。ReadTTYのエフェクトが投げられてきたらgetLineに、WriteTTYのエフェクトが投げられていたらputStrLnに処理を移譲する。これによって、単なる型シグネチャだけのインターフェースに過ぎなかったTeletypeに初めて、標準入出力を読み書きするという意味が割り当てられる。

各演算子の意味を具体的に説明しよう。

まず、f ~> gと書くと、これはforall x. f x -> g xと書いたのと同じことになる。なお、この演算子は->よりも強く結合する。エフェクトハンドラではこの形の型が頻出するので、この型シノニムは重要だ。展開すると、

teletypeToIO :: (IO <| r, ForallHFunctor eh) => (eh :!! LTeletype ': r) a -> (eh :!! r) a

ということだ。

次に、:!!。これが、Heftiaで中心的な役割を果たすものだ。
これはエフェクトフルなプログラムのモナドを表す。:!!の左側に高階エフェクト型の型レベルリストを、右側に一階エフェクト型の型レベルリストを書く。ただし注意として、いろいろな都合上、右側の一階エフェクトリストに要素としてTeletypeと直接書くことはできない。代わりに、Lを付けたLTeletypeと書く必要がある。これはmakeEffectF関数で自動生成されるもので、LiftIns Teletypeと書いても同じ意味になる。

':は実はHaskellが標準に用意しているもので、型レベルのリストの:（cons演算子）だ。

<|は、さっきの<:に似ているが、<:はキャリア型に対する制約なのに対して、こちらはエフェクト型の型レベルリストに対する制約だ。これはつまり、型レベルリストの変数rの中に要素としてIOモナドが存在しているということを表している。

最後にForallHFunctorだが、この制約があることでinterpretRec関数などの末尾にRecが付く関数が使えるようになる。あとの章に出てくるが、Recの付かない関数もある。Recを使用するほうがハンドラがより一般的になるので、使えるときは使うのが好ましい。具体的には、Recの付かないinterpretを使うと、高階エフェクトをすべて解釈し切った後にしかそのハンドラは使えなくなる。すなわち、先程は多相化されていたehだが、代わりに空のエフェクトリスト'[]しか受け付けなくなる:

teletypeToIO :: IO <| r => '[] :!! LTeletype ': r ~> '[] :!! r
teletypeToIO = interpret \case
    ReadTTY -> liftIO getLine
    WriteTTY msg -> liftIO $ putStrLn msg

Recが使えないケースについての説明はPart 2で行う。

エフェクトフルなプログラムの作成

次に、定義したエフェクトを使用するプログラムを書いてみよう。

echo :: (Teletype <: m, Monad m) => m ()
echo = do
    i <- readTTY
    case i of
        "" -> pure ()
        _ -> writeTTY i >> echo

このechoプログラムは、TTYに入力された文字列をオウム返しするループを行う。
ここで、もし空文字列が入力された場合（何も入力せずEnterキーが押された場合）、ループから脱出する。

型シグネチャにおいて:!!や<|を使用せずに<:のみを使用していることに気づくかもしれない。このように型シグネチャにおいてキャリアの具体的な形を指定しないことで、最も一般的な形でエフェクトフルプログラムを書けるようになる。いま制約として掛かっているのは、mがモナドであり、Teletypeのエフェクトをそこへ送信できるということだけだ。このことを「キャリアを多相化する」と呼ぶ。これによる効用は後に応用編にて解説できればと思う。

エフェクトフルプログラムをハンドラへ接続する

エフェクトフルなプログラムであるechoと、先程定義したteletypeToIOインタプリタを組み合わせて、実際に動くmain関数を構成してみよう。

import Control.Effect.ExtensibleFinal (runEff)

main :: IO ()
main = runEff do
    liftIO $ putStrLn "Please enter something..."
    teletypeToIO echo

runEff関数は、ハンドリングを繰り返して'[] :!! '[f]の形にまで縮小されたエフェクトフルプログラムについて、最後に残った唯一のエフェクト型fをキャリアと見なして（ここではf=IOモナド）、Heftiaの層である:!!を「脱皮」して単純なfだけにする操作だ:

runEff :: '[] :!! '[f] ~> f

これを実行し、適当に文字列をタイプすると、以下のようになる。
空文字列を入力した所で、プログラムが終了する。

Please enter something...
foo↵
foo
bar↵
bar
baz↵
baz
↵

解釈の改変

次に、interpose関数を使ったエフェクトの再解釈について見ていこう。
interpose系統の関数を使用すると、エフェクトを途中で別の解釈へと変更することができる。これはいわゆるプログラムのフックである。

あるいは、これは例外の再throwが近い。ここでは、例外がエフェクトであり、例外が湧いてくるコールスタックの深いところがエフェクトフルなプログラムであり、例外を投げることがエフェクトの送信であり、コールスタックの浅い所にある例外ハンドラがエフェクトハンドラに相当している。一度投げられた例外を、一旦catchして、その例外の内容に応じてまた別の例外を生成し、またthrowするのだ。

コンピューターネットワークに詳しい読者のために例えると、これはネットワークを流れるリクエストを中継するプロキシのようなものである。この例えにおいて、クライアントがエフェクトフルなプログラムであり、サーバーがハンドラ（インタプリタ）であり、エフェクトがリクエストであり、エフェクトの戻り値はレスポンスだ。再解釈系統の関数は、エフェクトフルなプログラムから送信されるエフェクトをその途中で受け取り、そのエフェクトの内容に応じた別のエフェクトフルプログラムを実行する。このプログラムにおいて、再度同じエフェクトを引数の内容だけ変えて再送信すると、あたかもクライアントからサーバーに送信されるリクエストを書き換えるプロキシのように動作することになる。

以下の関数は、Teletypeエフェクト型に関する挙動をフックするものである。
readTTYエフェクトについてはそのままの挙動が保たれる。一方、writeTTYエフェクトについては、元のwriteTTYの挙動を変更し、文字列の末尾にエクスクラメーションマークを付加する。

strong :: (Teletype <| ef, ForallHFunctor eh) => eh :!! ef ~> eh :!! ef
strong =
    interposeRec \case
        ReadTTY -> readTTY
        WriteTTY msg -> writeTTY $ msg <> "!"

この関数を使って、main関数を例えば以下のように変更する:

main :: IO ()
main = runEff do
    liftIO $ putStrLn "Please enter something..."
    teletypeToIO $ strong . strong $ echo

strongが2回適用されていることに注意してほしい。interposeはF ~> F形の型をもつ操作であるため、このように何度でも適用することができる。

実行結果は、以下のようになる。

Please enter something...
foo↵
foo!!
bar↵
bar!!
baz↵
baz!!
↵

なお、このようにエフェクトの引数の内容を書き換えるだけなら、より高速なtransform/translate/rewrite系関数を使用することが推奨される。今回の場合、strong関数は

import Control.Effect.Hefty (rewrite)

strong :: (Teletype <| ef, ForallHFunctor eh) => eh :!! ef ~> eh :!! ef
strong =
    rewrite \case
        ReadTTY -> ReadTTY
        WriteTTY msg -> WriteTTY $ msg <> "!"

と書き直すことができる。interpose系を使う場合との違いは、複数回に跨るような手続き的な処理へと再解釈できない点だ。例えば、受け取った一つのエフェクトを複数のエフェクトへと複製することはできない。

タグ付きエフェクト型

Heftiaは、Extensible Effects (EE) という方式に属するものだ。EEでは、エフェクト集合を表現するために型レベルのリストを使うことがある。この場合、同じエフェクト型をリスト内に複数回に出現させることもできる。

EEにおいて、エフェクトリスト内の要素であるエフェクト型は、おのおのがあたかもエフェクトを受け止める容器のように振る舞う。リスト内にエフェクト型が重複した状態の下でその型のエフェクトを投げると、リスト内で最も左（先頭側）にあるエフェクト型の容器にエフェクトは入る。あるいは先程のサーバー・クライアントのメタファーで言うと、リストのインデックス番号がサーバーのアドレスで、それぞれでハンドラたるサーバーのインスタンスが別々に起動しているイメージだ。このように、「エフェクトが入るところ」というイメージを込めて、エフェクトリスト内の要素ないしインデックスのことを（エフェクトの）スロットと呼び表すことにする。

例えば、'[] :!! '[A, B, C, D, D, D, E]というエフェクトリストの下でD型のエフェクトを投げると、インデックスが3番（0オリジン）のDにエフェクトは送られる。最も左側（アドレスが若い方）に送信されるというルールは、振る舞いが暗黙的なので、注意していないと間違ったところにエフェクトを送ってしまうかもしれない。さらに、4番や5番のDへエフェクトを送りたいという場合は、どうすればよいだろう？

そこで、エフェクト型には互いの識別のためのタグを別途付けることができる。これにより、リスト内に重複がある場合でも、ごちゃごちゃに混線してしまうことはないだろう。

タグは、'[] :!! '[A, B, C, D # "one", D # "two", D # "three", E]のように書く。
型レベル文字列以外にも任意の型レベルのものがタグとして使える。

以下は、ここまでのコードをタグ付けした例だ。
ただ、ここでは複数のTeletypeが出現することはないので、タグ付けするメリットは特にない。

import Data.Effect.Tag (Tag (unTag), type (#))
import Control.Effect.Hefty (untagEff)

echo :: (Teletype # "tty1" <: m, Monad m) => m ()
echo = do
    i <- readTTY' @"tty1"
    case i of
        "" -> pure ()
        _ -> writeTTY' @"tty1" i >> echo

strong :: (Teletype # "tty1" <| ef, ForallHFunctor eh) => eh :!! ef ~> eh :!! ef
strong =
    interposeRec @(_ # "tty1") \e -> case unTag e of
        ReadTTY -> readTTY' @"tty1"
        WriteTTY msg -> writeTTY' @"tty1" $ msg <> "!"

main :: IO ()
main = runEff do
    liftIO $ putStrLn "Please enter something..."
    teletypeToIO . untagEff @"tty1" . strong . strong $ echo

タグ付きエフェクト型の送信には、makeEffect系THが生成するアポストロフィの付いたバージョンの関数を使う。

untagEff関数は、エフェクトリストの先頭のタグ付けされたエフェクト型のタグを剥がす:

import Data.Effect (LiftIns)

untagEff :: eh :!! LiftIns (e # tag) ': r ~> eh :!! LiftIns e ': r

LiftInsは先程と同様、都合上のものなので無視してよい。

エフェクトの活用方法

ここまでで、Heftiaによるエフェクトの使用例を見てきた。
ここで着目するべきは、インタプリタであるteletypeToIOとエフェクトフルプログラムであるechoが定義として分離されている点だ。

このエコープログラムをCLIではなく何かGUIに組み込みたいとなったとき、TeletypeエフェクトをGUIに対する操作に変換するteletypeToGUIハンドラを後から書くことで、echo側を一切修正せずに目的を達成できる。

さらに、echoを書いている最中は、readTTYの裏でどのような処理が動くかについて一切気にする必要がない。これはつまり、ドメインロジック（ビジネスロジック）と、低水準で実装都合的でハードウェア的なインフラシステムとの間で分離ができているということを意味する。ドメインロジックとインフラシステムの間が、エフェクトという抽象化層、インターフェースによって接続されているのである。

このような分離は、現代において重要性が十分に認識されているので、既に実現するさまざまな方法がある。その中でもエフェクトパラダイムを使う利点は、ドメインロジックを表現するコードの可読性、合成可能性、モジュラー性だ。

十分に高度なEEにおいては、エフェクトを定義することはすなわちDSL（ドメイン特化言語）を定義することと等しい意味をもつ。そこで書かれるエフェクトフルプログラムは、ドメインロジックを表現するのに必要最小限な記述に絞られる。それはまさにそのドメイン専用に設計された言語を書いているという体験を可能にする。分離を実現するための従来のアドホックなデザインパターンによるコード上のノイズは、最小限に抑えられる。

さらに、エフェクトフルプログラムは合成可能だ。複数のエフェクトフルプログラムは、エフェクトシステムにより、単に従来の手続き型言語を書くようにするだけで、自然にエフェクトの集合が合成される。
先程、EEではエフェクト集合を表現するために型レベルのリストを使うと述べた一方で、<:を使用した形式で型シグネチャが書かれたエフェクトフルプログラムの例をエフェクトフルなプログラムの作成に示した。<:や<|を使用した制約でエフェクト集合を表現する場合、エフェクト集合の異なるエフェクトフルプログラム同士は自然に合成される。EEではエフェクト集合を表現するために、型レベルリストを使う他にこのようにHaskellの制約が暗黙的にANDで合成されていくのを利用することで、エフェクトの型システムをエミュレートできる。

最後に、モジュラー性。これは合成可能性の一種とも言える。エフェクトフルプログラムは、インタプリタによってエフェクトを解釈し、エフェクト集合を段階的に縮小していくことができる。つまり、あるソースコードの箇所で定義されたエフェクトフルプログラムである

prog :: ('[] :!! '[A,B,C]) a

を、まず別の箇所でその中の一つのエフェクト型Aを解釈してそれを

prog' :: ('[] :!! '[B,C]) a

と定義して、それをさらに別の箇所で今度は別のエフェクト型Cを解釈してそれを

prog'' :: ('[] :!! '[B]) a

として…というようなことが可能というわけだ（解釈するエフェクト型はリストの先頭に限られない。リストは自由に並び替えることができる）。さらに、ある箇所で定義されたプログラムを別の箇所で容易にフックできる利点は言うまでもない^[2]。

エフェクトパラダイムの欠点としては、先に述べた利点を実現するためには、高度な型システムとミニマルな言語構文・糖衣構文が要請される点である。これにより、主流の言語においてEEをライブラリとして実現するのは困難であり、単に同じ原理 (いわゆるFreer) を実現するように移植するだけでは十分な利便性は得られない。EEがHaskellにおいて盛んであるのは、単純にHaskellに実験的な文化のコミュニティが根付いているからという理由だけでなく、必要な要請を強く満たしていることがあるだろう。

まとめ

一階エフェクトの定義にはmakeEffectFを使う
エフェクトハンドラを作るにはinterpret系の関数を使う
エフェクトのフックにはintepose系の関数を使う
タグを付けることでリスト内で重複したエフェクト型をわかりやすく識別可能にできる
エフェクトパラダイムは、ドメインロジックを表現するコードの可読性、合成可能性、モジュラー性に優れている

次: Heftiaエフェクトシステムライブラリ入門 Part 2 - 高階エフェクト

コード全体

コードの全体は以下のようになる。タグ付きエフェクトのコードはGitHubにある。

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TemplateHaskell #-}

module Main where

import Control.Effect (type (<:), type (~>))
import Control.Effect.ExtensibleChurch (runEff, type (:!!))
import Control.Effect.Hefty (interposeRec, interpretRec)
import Control.Monad.IO.Class (liftIO)
import Data.Effect.TH (makeEffectF)
import Data.Hefty.Extensible (ForallHFunctor, type (<|))

data Teletype a where
    ReadTTY :: Teletype String
    WriteTTY :: String -> Teletype ()
makeEffectF [''Teletype]

teletypeToIO :: (IO <| r, ForallHFunctor eh) => eh :!! LTeletype ': r ~> eh :!! r
teletypeToIO = interpretRec \case
    ReadTTY -> liftIO getLine
    WriteTTY msg -> liftIO $ putStrLn msg

echo :: (Teletype <: m, Monad m) => m ()
echo = do
    i <- readTTY
    case i of
        "" -> pure ()
        _ -> writeTTY i >> echo

strong :: (Teletype <| ef, ForallHFunctor eh) => eh :!! ef ~> eh :!! ef
strong =
    interposeRec \case
        ReadTTY -> readTTY
        WriteTTY msg -> writeTTY $ msg <> "!"

main :: IO ()
main = runEff do
    liftIO $ putStrLn "Please enter something..."
    teletypeToIO $ strong . strong $ echo

脚注

https://hub.docker.com/r/lanexpr/heftia ↩︎
アスペクト指向と呼ばれるパラダイムと利点を共有している。 ↩︎

GitHubで編集を提案