SNatで書く型レベル自然数(base-4.18.0.0)

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

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

そんな時に、ひょんなことから[シングルトン型](https://zenn.dev/mod_poppo/books/haskell-type-level-programming/viewer/singletons)の存在を知り、さらにシングルトン型としての`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パッケージ](https://hackage.haskell.org/package/singletons)と共に2012年に導入されたようなのですが、EisenbergとWeirichによるとその起源は1994年の林晋の論文『[Singleton, Union, and Intersection Types for Program Extraction](https://doi.org/10.1006/inco.1994.1016)』(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`コンストラクタを用いた不正な値の製造を排除しています。

[ドキュメント](https://hackage.haskell.org/package/base-4.18.0.0/docs/GHC-TypeNats.html)にもありますが、パターンとしては`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
```
という[無を取得](https://dic.nicovideo.jp/a/%E7%84%A1%E3%82%92%E5%8F%96%E5%BE%97)みたいな型をしています。あまりにも非直観的ですね。

### 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`で書くことの恩恵は、次のような関数(値)が自然に書けるようになることだと考えています。
```Haskell
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](https://doi.org/10.1145/2364506.2364522)
[Draft version (pdf)](https://richarde.dev/papers/2012/singletons/paper.pdf)
- [GHCの型レベル自然数を理解する](https://qiita.com/mod_poppo/items/3a37424d299a9f71b757) (mod_poppo)
- [Haskellでの型レベルプログラミング](https://zenn.dev/mod_poppo/books/haskell-type-level-programming) (mod_poppo)