baseパッケージにある型レベルプログラミング探検の旅

　数学といえば定理証明。
コンピュータといえばHaskell。

ということでHaskellで定理証明（型レベルプログラミング）です！

　この記事は数学とコンピュータ Advent Calendar 2017の、
12月3日の記事です。

始まり

　多くのHaskellerは標準モジュールとしてbaseを利用していることかと思いますが、
baseパッケージにはいくつかの、型レベルプログラミングのためのモジュールが存在します。

• base - Stackage

　面白そうなので、探検していきます。
皆、定理証明が大好きだもんな！

Data.Type.Bool

　ハロー型レベル！

• Data.Type.Bool - Stackage

　皆さん割と型レベルifは書きたくなることが多いと思いますが、
実はbaseに定義されています。
使ってみましょう。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import Data.Type.Bool (If, type (&&), type (||), Not)

type X = If (Not 'False && 'False || 'True)
            Int
            Char

x :: X
x = 10

main :: IO ()
main = return ()

• Data.Type.Bool - Stackage

　これらはclosed type familyです。

以下のように「条件が正しいかに関わらずコンパイルが通るけど、
条件が正しいかによって変数xの型が変わる」
っていうものも作れます。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import Data.Type.Bool (If, type (&&), type (||), Not)
import Data.Functor.Const (Const)

type X = If (Not 'False && 'False || 'True)
            (Const Integer Char)
            Int

x :: X
x = 10

main :: IO ()
main = return ()

　これは余談ですが、
instance Num a => Const a bにより10 :: Const Integer Charなどのような型付けが正しいというのを、
僕が知った時もびっくりしました。
Constすげー。

Data.Type.Equality

(==)

　このtype (==)はカインド多相（PolyKinds）なので、
*カインドではない型も、以下に実装があれば比較ができます。

• Data.Type.Equality (==) - Stackage
  • 例えば以下の種に属する型は、標準的に比較できる
  • type (==) Bool a b
  • type (==) Ordering a b
  • type (==) * a b
  • type (==) Nat a b

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import Data.Type.Equality (type (==))

type X = Int == Char
type Y = Int == Int
type Z = 1 == 2

type A = [Int, Char] == [Int, Bool]
type B = (Int, Char) == (Int, Bool)

main :: IO ()
main = return ()

ghci

>>> :kind! X
X :: Bool
= 'False

>>> :kind! Y
Y :: Bool
= 'True

>>> :kind! Z
Z :: Bool
= Z

>>> :kind! A
A :: Bool
= 'False

>>> :kind! B
B :: Bool
= 'False

　(==)はopen type familyなので、自前の型の比較も定義できます。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import Data.Type.Equality (type (==))

data Foo = Bar | Baz

type family EqFoo (a :: Foo) (b :: Foo) :: Bool where
  'Bar `EqFoo` 'Bar = 'True
  'Baz `EqFoo` 'Baz = 'True
  a    `EqFoo` a    = 'False

type instance (a :: Foo) == (b :: Foo) = EqFoo a b

type X = 'Bar == 'Bar

main :: IO ()
main = return ()

• Data.Type.Equality - Stackage

　あとは色々や色々など、まだまだあります。

GHC.TypeLits

　これは最強です。
単純な依存型ならばsingletons使わないでこれだけでもいける。

---

baseではないので解説は省略しますが、singletonsはここにあります。

• Data.Singletons - Stackage

---

　GHC.TypeLitsは型レベル自然数（Natカインドとその型）と型レベル文字列（Symbolカインドとその型）へのユーティリティを提供します。

• GHC.TypeLits - Stackage

Nat, (+), (-), (*), (^)

　Proxy :: Proxy (1 + 2)という異常な式が書けます。
(/)はないです。
ユークリッドさんはいません！

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import Data.Proxy (Proxy(..))
import GHC.TypeLits (natVal)
import GHC.TypeLits (type (+), type (-), type (*)) -- ユークリッド感がない

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

x :: Integer
x = natVal (Proxy :: Proxy (1 + 2))

main :: IO ()
main = print x
-- {output}
-- 3

　自然数モノイドの法則を簡易的に確認とかできます。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import Data.Proxy (Proxy(..))
import Data.Type.Bool (type (&&))
import Data.Type.Equality (type (==))
import GHC.TypeLits (type (+))

type MonoidLaws =  0 + 1 == 1 && 1 == 1 + 0
               && (1 + 2) + 3 == 1 + (2 + 3)

x :: MonoidLaws ~ 'True => ()
x = ()

main :: IO ()
main = print x
-- {output}
-- ()

(~) :: k -> k -> Constraintについては、以下を参照。

• 番外編: (~)

Symbol

　Natと同じく、めちゃめちゃ応用性のあるやつ。

{-# LANGUAGE DataKinds #-}

import Data.Proxy (Proxy(..))
import GHC.TypeLits (Symbol, symbolVal)

x :: String
x = symbolVal (Proxy :: Proxy "sugar")

main :: IO ()
main = putStrLn x
-- {output}
-- sugar

　servantとかが利用してます。

• haskell-servant の利用例とちょっとだけ仕組みの調査 - KrdLab's blog
• servant - Stackage

TypeError

　Monadブレイカーの二つ名で知られている（いない）唯一無二の存在、error関数の型レベル版です。

　error関数は型を無視して例外投げる破壊者ですが、TypeErrorは誤った証明をコンパイルエラーに上げるだけなので、
安全です。

>>> :kind! TypeError
TypeError :: ErrorMessage -> b
= (TypeError ...)

（...は多分 深淵を表していて、僕のような並のHaskellerではたどり着けない魔法がかかっている気がします）

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits (TypeError, ErrorMessage(..))

type family Head (xs :: [k]) :: k where
  Head '[] = TypeError ('Text "an empty list is given")
  Head (x ': _) = x

x :: Head '[Int, Char, Bool]
x = 10

main :: IO ()
main = print x
-- {output}
-- 10

-- 以上省略 --

x :: Head '[] -- TypeError型の呼び出し
x = 10 -- ここが15行目

main :: IO ()
main = print x -- ここが18行目
-- Test.hs:15:5: error:
--     • an empty list is given
--     • In the expression: 10
--       In an equation for ‘x’: x = 10
-- 
-- Test.hs:18:8: error:
--     • an empty list is given
--     • In the expression: print x
--       In an equation for ‘main’: main = print x

(<=)

　なぜかこれだけConstraintです。
（(<=) :: (a :: Nat) -> (a :: Nat) -> Constraint）

多分Constraintで等価性調べるなら(~)でいいし、
<は本質的に(n - 1) <= mだからそれでどうぞ、ってことだと思う。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import GHC.TypeLits (type (<=))

x :: 2 <= 2 => ()
x = ()

main :: IO ()
main = print x
-- {output}
-- ()

-- 以上省略 --

x :: 3 <= 2 => ()
x = () -- 

main :: IO ()
main = print x
-- Test.hs:11:14: error:
--     • Couldn't match type ‘'False’ with ‘'True’
--         arising from a use of ‘x’
--     • In the first argument of ‘print’, namely ‘x’
--       In the expression: print x
--       In an equation for ‘main’: main = print x

めっちゃ便利そう。

(<=)をConstraintから型レベルに下げた、(<=?)というものあるみたいです。
あとは

余談

　これって-Woverlapping-patternsを警告されるだけで、コンパイルは通っちゃうんですね。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import GHC.TypeLits (type (<=))

x :: 3 <= 2 => ()
x = ()

main :: IO ()
main = return ()
-- Test.hs:8:1: warning: [-Woverlapping-patterns]
--     Pattern match is redundant
--     In an equation for ‘x’: x = ...

---

　あとは

• CmpNat (m :: Nat) (n :: Nat) :: Ordering
• CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering

とかあります。

• GHC.TypeLits

番外編: (~)

　(~)がどこから来てるのかわからないのでここに書いちゃいますが、
(~)はこういうのです。

>>> :kind (~)
(~) :: k -> k -> Constraint

>>> () :: 1 ~ 1 => ()
()

>>> () :: 1 ~ 2 => ()

<interactive>:11:1: error:
    • Couldn't match type ‘1’ with ‘2’
        arising from an expression type signature
    • When instantiating ‘it’, initially inferred to have
      this overly-general type:
        1 ~ 2 => ()
      NB: This instantiation can be caused by the monomorphism restriction.

>>> () :: 1 ~ 'True => ()

<interactive>:12:11: error:
    • Expected kind ‘ghc-prim-0.5.0.0:GHC.Types.Nat’,
        but ‘'True’ has kind ‘Bool’
    • In the second argument of ‘~’, namely ‘True’
      In an expression type signature: 1 ~ True => ()
      In the expression: () :: 1 ~ True => ()

　() :: () ~ () => ()ってすごい面白い式じゃないですか？
任意の式の中でも屈指の面白さだと思います。

終わり

　定理証明系Haskellや型レベルプログラミングとかいうと引く人が多いかもしれませんが、
実際問題「型レベルプログラミング実用的ではないのか？」というと、そんなことはないと思います。

例えばextensibleパッケージのここらへんが、いい感じに型レベルプログラミングを行っていると思います。
servantもかな？

• Data.Extensible.Internal - Stackage

しかし「コンパイルエラーが難解になる」という問題が（程度によって）あるので、トレードオフです。
そのパッケージの利便性がそのリスクを上回るのであれば、現実的だと思います。

参考ページ

• haskell/type-level-programming.md at master - lotz84/haskell - GitHub
• haskell-servant の利用例とちょっとだけ仕組みの調査 - KrdLab's blog