TL;DR

base-4.18.0.0でNat型のシングルトンであるSNatが実装され、型レベル自然数が扱いやすくてとても助かってます……base-4.18.0.0だって?

前置き

Haskellで型レベル自然数が扱えたら(特定目的に)捗るだろうなぁと前々から思っていたのですが、私は理論と実装の間のギャップで一番死ぬタイプなので、構想はありつつもうまいこと実装に落とし込めずにもやもやしていました。

そんな時に、ひょんなことからシングルトン型の存在を知り、さらにシングルトン型としてのNatの実装であるSNatが存在していることを知りました。これは以前からやりたかったことがこれで実装できるのでは？と思い嬉々として手を付け始めた次第です。←今ここ。

GHC.TypeNatsの実装

型レベルプログラミングにおいて例示的に実装される型レベルの自然数はペアノの公理を利用した、非常に理論書的な自然数です。計算機理論の論文なり教科書なりでも、自然数の実装がそうなっていることは多々見かけますので、これ自体は普通のことですね。

ですがペアノの公理を素朴に実装した自然数にはあからさまな問題が存在します。大きな自然数になるほどアホみたいな量のメモリを喰うことになるのです。
ですので、例えばGHCにおけるNaturalの定義は以下のようになっています。

GHC/Num/Natural.hs

data Natural
   = NS !Word#
   | NB !BigNat#

この結果、例えば型レベルプログラミングをGHC.TypeNatsで行おうと思った場合かなり面倒な事態に見舞われます(らしいです)。今のところ私自身は型レベルプログラミングまで踏み込む予定がないのでこれについては伝聞です。

シングルトン型

シングルトン型は「⊥でない値をただ1つもつ型」と形容されます(Eisenberg & Weirich, 2012より引用)。やってることはものすごく単純であり、つまりその型に対応する値をただ1つだけ所持しています。今回の場合だと、SNat n型の値はnのみであると要請されます。これにより、型レベルの自然数と値レベルの自然数が意味上接続され、型と値の間の架け橋となります。

Haskellにはおそらくsingletonsパッケージと共に2012年に導入されたようなのですが、EisenbergとWeirichによるとその起源は1994年の林晋の論文『Singleton, Union, and Intersection Types for Program Extraction』(Information and Computation, vol. 109(1–2), pp.174–210) まで遡れるそうです。

base-4.18.0.0

前置きもええ加減にしてさっそくSNatを触っていきたいところですが、これが実装されたのはbase-4.18.0.0だというところに1つ注意点があります。つまり、最新パッケージにしか実装されていません。StackageのLTSに頼り切っていた私のような怠け者には辛い、configurationからいじる時間のはじまりです。

いやまあ、

stack.yaml

resolver: ghc-9.6.1

を設定してghc-9.6.1と対応するHLSをインストールすれば済む話なのですが。

SNat値の取得

SNat n型は実装上以下のような形で定義されています。

GHC/TypeNats.hs

newtype SNat (n :: Nat) = UnsafeSNat Natural

ですがこの名前から安全でなさそうな型コンストラクタは使いません(そもそも使うことを許されていませんが)。SNatの値を得たり使ったりする際は、3つの異なる方法が用意されています。

KnownNatによる取得

SNatの実装に合わせて、KnownNatクラスが内部的に持っていたメソッドnatSingが公開のものに変更されました。従ってKnownNat n制約の下では、natSingと書くだけで対応するSNat n型の値を取得できます。

GHC/TypeNats.hs

class KnownNat (n :: Nat) where
  natSing :: SNat n

SNatパターンによる取得・パターンマッチ

GHC.TypeNatsではパターンシノニムとしてのSNat nを用意しています。

GHC/TypeNats.hs

pattern SNat :: forall n. () => KnownNat n => SNat n
pattern SNat <- (knownNatInstance -> KnownNatInstance)
  where SNat = natSing

(06.18改稿)
パターンシノニムを用いることで、KnownNat n制約とSNat n型の相互変換を実現しており、またSNatを経由させることでUnsafeSNatコンストラクタを用いた不正な値の製造を排除しています。

ドキュメントにもありますが、パターンとしてはf SNat = ...のように記述され、式としてはSNat @n :: KnownNat n => SNat nのように使われます。nが明らかであれば型適用も不要になります。

withSomeSNat関数

GHC/TypeNats.hs

withSomeSNat :: forall rep (r :: TYPE rep).
                Natural -> (forall n. SNat n -> r) -> r
withSomeSNat n k = k (UnsafeSNat n)

withSomeSNat関数はNatural型の値をSNat n型に持ち上げるときに使います。仕様上実行時までnが決定できないため、継続渡しの形で実装されています。
SNatを利用した自作の型の値を得るときにもwithSomeSNatを使用します。(後述)

Naturalへの変換

Natカインドから値を取得するためにはnatVal関数を使いますが、この関数はn::Natを確保するためなのかなんなのか、

GHC/TypeNats.hs

natVal :: forall n proxy. KnownNat n => proxy n -> Natural

という無を取得みたいな型をしています。あまりにも非直観的ですね。

fromSNat関数

SNat n型が値としての自然数も所持しているため、その取得が圧倒的に簡単かつ直観的になりました。

GHC/TypeNats.hs

fromSNat :: SNat n -> Natural

とてもうれしいですね。

実践：有界な自然数の型

SNat nの実践として、有界な自然数の型FinNat nを実装してみます。これ自体はあまり大したことができないのですが、今後やってみたいことの前段階のさらに下準備みたいな感じです。

Some.hs

{-# LANGUAGE KindSignatures #-}

data FinNat (n :: Nat) = FN Natural (SNat n)

FinNat n型は最大値 $n-1$ の自然数の型を想定しています。つまり、Word8とFinNat 256が集合として同型になるようなイメージです。

これをSNatで書くことの恩恵は、次のような関数(値)が自然に書けるようになることだと考えています。

zero :: forall n. (KnownNat n, (1::Nat) <= n) => FinNat n
zero = FN 0 natSing

boundNat :: FinNat n -> Natural
boundNat (FN _ x) = fromSNat x

FinNat nは現在のところ、Eq, Ord, Boundedのインスタンスを獲得しています。

Some.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

instance Eq (FinNat n) where
  FN x _ == FN y _ = x == y

instance Ord (FinNat n) where
  FN x _ <= FN y _ = x <= y

instance (KnownNat n, (1::Nat) <= n) => Bounded (FinNat n) where
  minBound = zero
  maxBound = FN mo natSing
    where
      mo = natVal (Proxy :: Proxy n) - 1

FinNat n型の値を作るときは、存在型SomeFinNatを経由することになります。

Some.hs

{-# LANGUAGE ExistentialQuantification #-}

data SomeFinNat = forall n. SomeFinNat (FinNat n)
someFinNat :: (Integral a, Integral b) => a -> b -> Maybe SomeFinNat
someFinNat i n | n <= 0                     = Nothing
               | i <  0                     = Nothing
               | toInteger n <= toInteger i = Nothing
               | otherwise                  = Just $ withSomeSNat (fromIntegral n) (\sn->SomeFinNat (FN (fromIntegral i) sn))

(06.18追記)
不正な値が作られることを阻止するため、SNat同様パターンシノニムを導入しました。

Some.hs

import qualified Some.Exception as E -- 例外データの定義

data FinNat (n :: Nat) = FN Natural (SNat n)
pattern FNat :: Natural -> SNat n -> FinNat n
pattern FNat i sn <- FN i sn
  where
    FNat i sn | fromSNat sn <= i = E.throw E.ValueOverflow         -- 数値が境界を越えている
              | fromSNat sn <= 0 = E.throw E.NonPositiveUpperBound -- 境界値が0以下である
              | otherwise        = FN i sn

参考文献

Eisenberg, Richard A., Weirich, Stephanie (2012). Dependently Typed Programming with Singletons. Haskell '12: Proceedings of the 2012 Haskell Symposium. pp.117–130 doi:10.1145/2364506.2364522
Draft version (pdf)
GHCの型レベル自然数を理解する (mod_poppo)
Haskellでの型レベルプログラミング (mod_poppo)