関数に多相的なリストを適用する

  • 10
    いいね
  • 2
    コメント
この記事は最終更新日から1年以上が経過しています。

前の記事 http://qiita.com/philopon/items/99760c65bcc2d3fcc4c1 では宣伝に終始したので、実装について触れたいと思います。

-- 脳内型あわせしてる部分があるので、型が合わなかったらghcより分かりやすいエラーメッセージでこっそり教えてください
-- 理解が追いついてないところも多々あるので間違えていたらツッコミお願いします。

はじめに

実現したいことはこんな感じです。

目標
app = do
    action $ do -- フィルタしなければ0引数
        doSomething

    filterA $ do -- フィルタして結果(Int)をsnoc
        filterB $ do -- フィルタするが結果は変えない
            filterC $ do    --- フィルタして結果(DoubleとString)をsnoc

                action $ \int double string -> do   -- 3つの引数が渡される!
                    doSomething

filter群はReaderモナドのlocal関数の様な処理で実現出来そうですが、

擬似コード
filter :: (多相リスト -> 多相リスト') -> Filter 多相リスト' -> Filter 多相リスト

action部分ではfilter群の結果の多相かつ任意の長さのリストを関数に適用する必要があります。
つまり、以下の様な関数を定義できれば上記の目標を達成できそうです。

目標',擬似コード
-- []は多相リスト

apply doSomething1 [] = doSomething
apply doSomething2 [1 :: Int, 2 :: String] = doSomething 1 2

以下のGHC拡張が必要です。ghc7.4以降で動くと思います。

haskell
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

多相リストの定義

まず、以下のようなシングルトンリスト(でいいのかな)を定義します。

haskell
data SList :: [*] -> * where
    SNil  ::                  SList '[]
    (:::) :: a -> SList xs -> SList (a ': xs)

infixr 5 :::

ghciで試してみると、consした値の型がSListの型レベルリストに保持されていることがわかります。

ghci
> :t SNil
SList '[]
> :t (1::Int) ::: SNil
SList '[Int]
> :t ("foo" :: String) ::: (1::Int) ::: SNil
SList '[String,Int]

関数に適用

これを関数に適用したいので以下のような関数を書きますが、このままでは型が合わず、エラーになります。

haskell
apply v SNil = v
apply f (a ::: as) = apply (f a) as

第一引数には任意の数の引数を取る関数が入り、そのままでは型を書けないためです。

擬似コード
apply :: ?? -> SList as -> r    -- ?? には任意の個数/型の引数を持つ関数が入る

しかし、第二引数のリストと戻り値に型の情報があるので、そこから第一引数の型を導けば良いのです。

擬似コード
applyA :: ?? -> SList '[Int,Int] -> Int -- ならば??はInt -> Int -> Intとなる。

型を返す関数は型族(type family)で定義できます。この関数の第一引数を満足させるには以下のように定義すれば良さそうですね。

haskell
type family Fn (as :: [*]) r
type instance Fn '[] r = r
type instance Fn (x ': xs) r = x -> Fn xs r

これを用いて、上記の例に型シグニチャを追加してあげれば

haskell
apply :: Fn xs r -> SList xs -> r
手動簡約
apply (+) ((1::Int) ::: (2::Int) ::: SNil)

{- 第一引数 :: Fn '[Int,Int] r
    = (Int -> Fn '[Int] r)
    = (Int -> Int -> Fn '[] r)
    = (Int -> Int -> r)

    (+)と型が合う!-}

= apply ((+) (1::Int)) ((2::Int) ::: SNil)

-- 第一引数 :: Fn '[Int] r = (Int -> r)

= apply ((+) (1::Int) (2::Int)) SNil

-- 第一引数 :: Fn '[] r = r

= ((+) 1 2)

= 3

と言う風にちゃんと型を付けられるので上手くいきます。

他にも実行例を挙げておきます

ghci
> apply (+) (3 ::: SNil) (8::Int) -- 第一引数のみをリストから適用、(Num a => a -> a)を返し、普通にIntを適用
11
> apply (+) (3 ::: 7 ::: 8 ::: SNil) -- 数字に数字を適用しようとするため当然エラー

<interactive>:6:1:
    Could not deduce (Num (a0 -> r))
      arising from the ambiguity check for ‘it’
    from the context (Num (a -> r), Num a)
      bound by the inferred type for ‘it’: (Num (a -> r), Num a) => r
      at <interactive>:6:1-34
    The type variable ‘a0’ is ambiguous
    When checking that ‘it’
      has the inferred type ‘forall r a. (Num (a -> r), Num a) => r’
    Probable cause: the inferred type is ambiguous

これでシングルトンリストを関数に適用出来るようになりました!

Snoc関数も定義しておきましょう。どちらも

haskell
type family Snoc (as :: [*]) a :: [*]
type instance Snoc '[] a = a ': '[]
type instance Snoc (x ': xs) a = x ': Snoc xs a

sSnoc :: SList as -> a -> SList (Snoc as a)
sSnoc SNil a = a ::: SNil
sSnoc (x ::: xs) a = x ::: sSnoc xs a

型がちゃんと付くか追ってみましょう

手動簡約
: sSnoc (13 ::: "t" ::: SNil) 4.1

{- 戻り値: SList (Snoc '[Int, String] Double)
= SList (Int ': Snoc '[String] Double)
= SList (Int ': String ': Snoc '[] Double)
= SList (Int ': String ': '[Double])

-- 末尾にDoubleが追加されている!
-}

= 13 ::: sSnoc ("t" ::: SNil) 4.1

-- 戻り値: SList (Snoc '[String] Double) = SList (String ': '[Double])

= 13 ::: "t" ::: sSnoc SNil 4.1

-- 戻り値: SList (Snoc '[] Double) = SList '[Double]

= 13 ::: "t" ::: 4.1 ::: SNil

ちゃんと型が付いていますね。
(当然ですが)型関数と関数が全く同じ形をしているのも面白いのではないでしょうか。

Constraintカインド

これでやりたいことは実現出来たのですが、SListはShowのインスタンスではありませんので、当然showする事が出来ず、デバッグとかでちょっと困ります。

ghci
(3::Int) ::: SNil

<interactive>:3:1:
    No instance for (Show (SList '[Int])) arising from a use of ‘print’
    In a stmt of an interactive GHCi command: print it

コレをShowのinstanceにしようとすると、リスト内の全ての要素がShowのinstanceであることを表さなければなりません。

このような制約を付けるためにはConstraintカインドを用いることが出来ます。

前準備として更に拡張を追加し、Constraintをimportしましょう

haskell
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE StandaloneDeriving #-}

import GHC.Exts(Constraint)

Constraintカインドは複数の制約をタプルで表します。
リスト中の全ての要素に対する制約は以下の様に書けます。

haskell
type family All (c :: * -> Constraint) (as :: [*]) :: Constraint
type instance All c '[] = ()
type instance All c (a ': as) = (c a, All c as)

型を合わせてみましょう。

手動簡約
All Show '[Int, Double]
= (Show Int, All Show '[Double])
= (Show Int, (Show Double, All Show '[])
= (Show Int, (Show Double, ()))

このように、要素中の全ての要素(Int,Double)に対してShow制約を付けられました!

あとはこれを用いてShow instanceを導出すれば

haskell
deriving instance All Show as => Show (SList as)
ghci
> ("test"::String) ::: (3::Int) ::: SNil
"test" ::: (3 ::: SNil)

このようにちゃんとshow出来るようになりました!

おわりに

型レベルプログラミング、参考記事読んで以来、すげーかっこいい感じだし使ってみたいなーって思っていたものの、イマイチ使いどころがわからずアレだったのですが、今回初めて便利っぽく使う事が出来たと思います。

内容的には全て参考記事に書いてあることなので、参考記事を読みましょう!

参考

GHC 7.4.1 の型レベル新機能を使い倒す 〜GADTs、型族 と DataKinds、ConstraintKinds の円環〜 - これは圏です