👀
型レベル数独チェッカー in Haskell
なんか見たので気まぐれに。
使用したghcは9.10.1.
GHCの型システムは、UndecidableInstances を指定すれば型関数内部で型関数を呼べるようになったりしてチューリング完全になります。普段は止まるはず。
型レベルチェッカー実装自体はそんなに難しくないのだけど、 (:~:) とか testEquality を使ったこと無かったのでその辺の知見が少し増えた。
たとえば以下のような関数を作ろうとしたけど、この型チェックが通らない。
sudoku ::
forall (nss :: List (List Char)) ->
IO ()
-- MEMO: nssは引数で渡されており、`Sudoku nss`の評価を静的に出来ない
sudoku nss = case testEquality (typeRep @(Sudoku nss)) (typeRep @True) of
Just Refl -> putStrLn "OK!!"
Nothing -> putStrLn "Failed!!"
これは型を渡して実行時にOKかどうか表示する関数のつもりだ。
ここで Sudoku :: List (List Char) -> Bool は型関数。nssは引数で渡されているから、具体的な形は決まらない。testEquality は型が同値かどうか(静的に)チェックする関数だが、具体的な形が決まらない型の比較は出来ない。なのでこのようなsudoku関数は型検査を通すことは出来ない。
まあ考えてみるとそれはそう、という感じなんだが、型レベル関数が絡むと関数のラッパーが簡単に作れなくなるのは大変だね。ラッパー関数はユーザーへのUIとしての関数を作る際に作ることが多いから。
そういえばTypeScript, Scala3ではUnion Typeがあるからplaceholderの扱いが簡単なんだけど、Haskellでは存在しないため、Char を使って誤魔化すことにした。
あと今Bool返しているけど、失敗時に TypeError を返すようにすればコンパイルエラーを返すことも出来る(コード内でコメントで示している)。
#!/usr/bin/env cabal
{- cabal:
build-depends: base
ghc-options: -Wall -Wno-overlapping-patterns -Wno-inaccessible-code
-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
--import GHC.TypeLits
import GHC.Exts (List)
import Data.Type.Equality ((:~:)(..), testEquality)
import Type.Reflection (typeRep)
type CheckDigit :: Char -> Bool
type family CheckDigit n where
CheckDigit '_' = True -- placeholder
CheckDigit '1' = True
CheckDigit '2' = True
CheckDigit '3' = True
CheckDigit '4' = True
CheckDigit '5' = True
CheckDigit '6' = True
CheckDigit '7' = True
CheckDigit '8' = True
CheckDigit '9' = True
CheckDigit _ = False -- TypeError ('Text "!!! Sudoku: Unexpected digit found")
type Unique :: List Char -> Bool
type family Unique xs where
Unique '[] = True
Unique (x : xs) = CheckDigit x && NotElem x xs && Unique xs
type NotElem :: Char -> List Char -> Bool
type family NotElem x xs where
NotElem _ '[] = True
NotElem '_' _ = True
NotElem x ('_' : xs) = NotElem x xs
NotElem x (x : xs) = False -- TypeError ('Text "!!! Sudoku: duplicate element found")
NotElem x (y : xs) = NotElem x xs
type (&&) :: Bool -> Bool -> Bool
type family (&&) x y where
(&&) False _ = False
(&&) _ y = y
type Sudoku :: List (List Char) -> Bool
type family Sudoku nss where
Sudoku [
[e11, e12, e13, e14, e15, e16, e17, e18, e19],
[e21, e22, e23, e24, e25, e26, e27, e28, e29],
[e31, e32, e33, e34, e35, e36, e37, e38, e39],
[e41, e42, e43, e44, e45, e46, e47, e48, e49],
[e51, e52, e53, e54, e55, e56, e57, e58, e59],
[e61, e62, e63, e64, e65, e66, e67, e68, e69],
[e71, e72, e73, e74, e75, e76, e77, e78, e79],
[e81, e82, e83, e84, e85, e86, e87, e88, e89],
[e91, e92, e93, e94, e95, e96, e97, e98, e99]
] =
-- Row check
Unique [e11, e12, e13, e14, e15, e16, e17, e18, e19]
&& Unique [e21, e22, e23, e24, e25, e26, e27, e28, e29]
&& Unique [e31, e32, e33, e34, e35, e36, e37, e38, e39]
&& Unique [e41, e42, e43, e44, e45, e46, e47, e48, e49]
&& Unique [e51, e52, e53, e54, e55, e56, e57, e58, e59]
&& Unique [e61, e62, e63, e64, e65, e66, e67, e68, e69]
&& Unique [e71, e72, e73, e74, e75, e76, e77, e78, e79]
&& Unique [e81, e82, e83, e84, e85, e86, e87, e88, e89]
&& Unique [e91, e92, e93, e94, e95, e96, e97, e98, e99]
-- Column check
&& Unique [e11, e21, e31, e41, e51, e61, e71, e81, e91]
&& Unique [e12, e22, e32, e42, e52, e62, e72, e82, e92]
&& Unique [e13, e23, e33, e43, e53, e63, e73, e83, e93]
&& Unique [e14, e24, e34, e44, e54, e64, e74, e84, e94]
&& Unique [e15, e25, e35, e45, e55, e65, e75, e85, e95]
&& Unique [e16, e26, e36, e46, e56, e66, e76, e86, e96]
&& Unique [e17, e27, e37, e47, e57, e67, e77, e87, e97]
&& Unique [e18, e28, e38, e48, e58, e68, e78, e88, e98]
&& Unique [e19, e29, e39, e49, e59, e69, e79, e89, e99]
-- 3x3 block check
&& Unique [e11, e12, e13, e21, e22, e23, e31, e32, e33]
&& Unique [e14, e15, e16, e24, e25, e26, e34, e35, e36]
&& Unique [e17, e18, e19, e27, e28, e29, e37, e38, e39]
&& Unique [e41, e42, e43, e51, e52, e53, e61, e62, e63]
&& Unique [e44, e45, e46, e54, e55, e56, e64, e65, e66]
&& Unique [e47, e48, e49, e57, e58, e59, e67, e68, e69]
&& Unique [e71, e72, e73, e81, e82, e83, e91, e92, e93]
&& Unique [e74, e75, e76, e84, e85, e86, e94, e95, e96]
&& Unique [e77, e78, e79, e87, e88, e89, e97, e98, e99]
Sudoku _ = False
type SudokuWIP :: Bool
type SudokuWIP = Sudoku [
['_', '3', '_', '_', '_', '_', '_', '_', '_'],
['_', '_', '_', '1', '9', '5', '_', '_', '_'],
['_', '_', '8', '_', '_', '_', '_', '6', '_'],
['8', '_', '_', '_', '6', '_', '_', '_', '_'],
['4', '_', '_', '8', '_', '_', '_', '_', '1'],
['_', '_', '_', '_', '2', '_', '_', '_', '_'],
['_', '6', '_', '_', '_', '_', '2', '8', '9'],
['_', '_', '_', '4', '1', '9', '6', '3', '5'],
['_', '_', '_', '_', '_', '_', '_', '7', '4']
]
main :: IO ()
main = do
case testEquality (typeRep @SudokuWIP) (typeRep @True) of
Just Refl -> putStrLn "OK!!"
Nothing -> putStrLn "Failed.."
Discussion