型チェックされた空ではない文字列

この記事はHaskellコアンです。背景と動機については後述しますが、ここでの目的は、私たちが採用し、楽しんでいる小さく珍しいテクニックを共有することです。これは完璧なブログネタです。要するに、私たちは型チェックされた空ではない文字列コンストラクタを作成し、数千に及ぶ同等のTemplateHaskellの呼び出しを置き換え、その結果、多くの呼び出しを行っていた大規模でデータ量の多いパッケージでビルド時間が約10%改善しました。 before, after, invalidBefore, invalidAfter :: NonEmptyText before = $$(NonEmptyText.make "hello") after = NonEmptyText.make "hello" invalidBefore = $$(NonEmptyText.make "") -- ⇝ スプライス評価中にエラー ... invalidAfter = NonEmptyText.make "" -- ⇝ 型エラー: 空ではない文字列が期待されます Bellroyのソフトウェアにおける核となる設計目標は、無効な状態を表現できないようにすることです。そのことを念頭に置いて、私たちがテキストデータ（非常に多い）によく使用する型はNonEmptyTextです。これは文字通り、少なくとも1文字の文字列を表す型です。このテクニックは、過去15年ほどのGHCの機能の集大成です。特に、GHC 9.10で導入されたRequiredTypeArgumentsにより、型レベルの文字列リテラルを値のように関数に渡すことができます。型レベルで空文字列を検出した場合、「空ではない文字列が期待されます」のようなカスタム型エラーメッセージを表示することができます。以下のようにです。 type family IsNonEmptySymbol symbol :: Constraint where IsNonEmptySymbol "" = Unsatisfiable (Text "Expected a non-empty string") IsNonEmptySymbol _ = (()::Constraint) -- 空の制約は常に満たされる -- RequiredTypeArgumentsがない場合の以前の構文に注意: -- make :: forall symbol. IsNonEmptySymbol symbol => NonEmptyText -- `make @"hello!"` のように使用 make :: forall symbol -> (IsNonEmptySymbol symbol) => NonEmptyText make symbol = NonEmptyText (fromString (symbolVal (Proxy :: Proxy symbol))) test :: NonEmptyText test = make "hello!" 適切なLANGUAGEプラグマがあれば、これは実際に機能します。これにはUndecidableInstancesが必要ですが、それ自体は有害ではありませんが、何が問題になりうるかという可能性を開きます1。さらに、IsNonEmptySymbolは型族であるため、通常の型クラス制約のように直接使用することはできません。例えば、Dictにパッケージ化したり、Data.SOP.hcfoldMapのような関数で使用したりすることはできません。Constraintを返しますが、通常の型クラスのように「インスタンスを要求する」ことはできません。このトリックの最後のステップは、IsNonEmptySymbolを型クラスとして記述することです。 class IsNonEmptySymbol symbol instance {-# OVERLAPPING #-} Unsatisfiable (Text "Expected a non-empty string") => IsNonEmptySymbol "" instance IsNonEmptySymbol a -- make: 上記と同じ make :: forall symbol -> (IsNonEmptySymbol symbol) => NonEmptyText make symbol = NonEmptyText (fromString (symbolVal (Proxy :: Proxy symbol))) GHCが空文字列に対してIsNonEmptySymbol制約を解決するとき、両方を見つけます。 _ => instance IsNonEmptySymbol "" と instance IsNonEmptySymbol a. OVERLAPPINGプラグマを省略すると、GHCがエラーを発生させるポイントになります。どちらのインスタンスを選択すべきかわからず、重複する可能性があると文句を言うでしょう。これは問題ありません。なぜなら、重複するインスタンスがある唯一のケースは、入力が「」の場合、つまり禁止したいケースだからです。したがって、ここでのOVERLAPPINGプラグマの効果は、GHCが「望む」インスタンス、つまりカスタム型エラーのあるインスタンスを選択することです。そのインスタンスは、ユーザーに空ではない文字列が期待されることを知らせるカスタムエラーメッセージを発生させます。 影響 当社の内部bellroy-dataパッケージ（既知の貨物および配送業者、会計システム、製品データ、税コードなどの情報を含む）には、$$(NonEmptyText.makeTH _)のようなTHスプライスが何千もありました。RequiredTypeArgumentアプローチに移行することで、そのパッケージのコンパイル時間が約10%短縮されました。 このトリックを適用できる類似のケース ほぼ同じコードを再利用して、特定のNatural数が正であることを検証し、型チェックされたPositiveコンストラクタを作成できます。一般的に、型レベルの述語を定義できる任意の型に対して、このテクニックを使用できます。ここから、例えばURIを構築するための型安全な用語構文を定義するために型レベルの文字列解析を想像できるかもしれませんが、これは機能しますが、すぐにGHCのデフォルトの削減制限である20にぶつかるでしょう。n長の文字列に対するO(n)の型レベルバリデータは、20の「削減」（つまり解析）ステップに厳密な上限があり、したがって解析は20文字を超えて進むことはできません。これは、解析ステップ自体がその制限にカウントされないと仮定した場合でもです。一般的に、非自明なアルゴリズムを型族で表現するのは非常にぎこちないです。例えば、let-bindingsを記述する方法がなく、caseのような構文でパターンマッチングを行うこともできません。これらが必要な場合は、追加の型引数とヘルパー型族の組み合わせで表現する必要があります。また、上記のIsNonEmptySymbolクラスのように型クラスとして機能させるためには、多少の配管作業も必要です。それでも、ここまで読み進めたあなたは、それがどのように見えるか興味があるかもしれません。 DynamoDBテーブル名の型レベル解析をご覧ください。 {-# LANGUAGE DataKinds #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RequiredTypeArguments #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} import Data.Proxy import Data.String (fromString) import Data.Text (Text) import Data.Type.Bool qualified as Bool import GHC.TypeError import GHC.TypeLits -- | 有効なDynamoDBテーブル名は正規表現 /^[a-zA-Z_.-]{3,255}$/ に一致する必要があります newtype TableName = TableName Text deriving (Show) make :: forall name -> (IsValidTableName name) => TableName make name = TableName (fromString (symbolVal (Proxy :: Proxy name))) ここまでは順調です。しかし、すべての無効な文字列を列挙するには時間がかかります。上記のIsNonEmptySymbolが機能したようなアルゴリズム的なアプローチが必要です。上記と同様に、これをType -> Constraintの種類の型クラスにカプセル化することを好みます。ここで使用するアプローチは、型族を使用して内部型クラスの解決を指示することです。したがって、このアプローチは単項型クラスとして機能し（望ましい）、プログラマーにカスタム型エラーメッセージを表示します（素晴らしい）。 class (KnownSymbol a) => IsValidTableName a instance (KnownSymbol a, IsValidTableName_ validity a) => IsValidTableName a -- | 素敵なエラーメッセージを生成するラッパークラス -- -- `wasValid`パラメータは`IsValidTableName__`型族によって計算されます。 -- その後、GHCをno-opインスタンス（成功）またはやや情報的なエラーをスローするインスタンスに指示できます。 class (IsValidTableName__ a ~ wasValid) => IsValidTableName_ (wasValid :: Bool) a instance (IsValidTableName__ a ~ 'True) => IsValidTableName_ 'True a instance (Unsatisfiable ('Text "Encountered invalid TableName")) => IsValidTableName_ 'False a さて、IsValidTableName__ (input :: Symbol) :: Bool というIsValidTableName__型族を実際に実装する必要があります。 type IsValidTableName__ text = IsValidTableName_go 0 'Nothing (UnconsSymbol text) -- IsValidTableName__型族の内部ループ type family IsValidTableName_go (len :: Nat) (invalidLastChar :: Maybe Char) (unconsResult :: Maybe (Char, Symbol)) :: Bool where IsValidTableName_go len 'Nothing ('Just '(x, xs)) = IsValidTableName_go (len + 1) (InvalidTableChar x) (UnconsSymbol xs) IsValidTableName_go len 'Nothing _ = (3 <=? len) Bool.&& (len <=? 255) IsValidTableName_go len ('Just invalidChar) _ = 'False -- 個々の文字の有効性をチェック type family InvalidTableChar (ch :: Char) :: Maybe Char where InvalidTableChar ch = Bool.If (IsValidTableChar ch) 'Nothing ('Just ch) type family IsValidTableChar (ch :: Char) :: Bool where IsValidTableChar '-' = 'True IsValidTableChar '_' = 'True IsValidTableChar '.' = 'True IsValidTableChar ch = ('a' <=? ch Bool.&& ch <=? 'z') Bool.|| ('A' <=? ch Bool.&& ch <=? 'Z') Bool.|| ('0' <=? ch Bool.&& ch <=? '9') 最後に、