古い上に目的を達成させられなかった挫折ゴミ記事です。読んでも時間の無駄だと思います。(2016/12 追記)
概要
Haskellで関数内で型指定する方法について調べたことのメモです。「asTypeOfをもうちょい使いやすくできないか？」が主なテーマです。asTypeOf自体の説明やtype scoped variableについては触れません。この辺りのキーワードについてはこのページが大変参考になりました。GHCは7.8以降、baseは4.8以降を対象にしてます。
注意
私は新参haskellerです。Haskellは3月から日曜プログラミングで使い始めて何とか使えるようになったレベルで、まだまだ分からないことだらけです。とはいえまぁせっかく調べたし、Qiitaとか一度は使ってみたいし、もしかしたら偉い人がよりエレガントな方法を教えてくれるかもしれない、みたいな動機で書いてます。
動機
具体的に何がしたいかについて述べます。
例えば、以下のようなバイナリファイルからrepaのArrayを読み込んで絵として表示するようなプログラムがあったとします。
readImage :: FilePath -> Int -> Int -> Int -> IO (Array REF.F DIM3 a)
readImage = 略
drawImage = do
image <- (readImage "hoge.raw" 100 100 1 :: IO (Array REF.F DIM3 Word8) ) -- 100 x 100
draw image
コンパイラに教えるべき情報って a が Word8であることだけなのに沢山書かなきゃいけないですね。そこでasTypeOfを少しいじって使えば以下のように書けないか、というのが発端となるアイデアです。
drawImage = do
image <- readImage "hoge.raw" 100 100 1 `as` (tp2.tp0) $ (0 :: Word8)
draw image
はっきりいってそんなに短くなってないのであまり嬉しくないと感じるかもしれませんが、型を調べる手間が省けたり、より抽象的に書けたりするメリットがあります（と期待して作り始めたものの自信なくなってきた・・orz）
少しコードについて補足します。まずasはasTypeOfの拡張でas :: a -> (a->b) -> b -> aという型を制限する為の関数です。tp0やtp2は数字に対応する型パラメータを抜き出す関数です。この例ではtp0 :: f a -> aでIOを取り除いて、tp2 :: f a b c -> cで束縛したい型を取り出してます。今回のRepaのArrayは型パラメータを３つとるデータ族ですが、実際には１つの関数で型パラメータの数が幾つでも対応できる方が望ましいです。つまり型族使って何とかしたいです。Template Haskellでもできたんですけどreifyする為に一度変数に束縛しないといけないとか、$() 気持ち悪いとかいう理由でやめました。こちらも詳しい人に聞いたら良い方法があるかもしれません。
7/6追記:
最後の0 :: Word8というマジックナンバーは型を指定する為のもので、値は意味ないです。
結果
結論から言うと、上の目標は達成できませんでした。tp2.tp0という所でコンパイラに怒られます。一応エラーメッセージをのせておくと、後述するGetTPという型族が評価されず、マッチングに失敗します。
Couldn't match type ‘GetTP (Array REF.F DIM3 e0) 2’ with ‘Word16’
The type variable ‘e0’ is ambiguous
Expected type: Array REF.F DIM3 e0 -> Word16
Actual type: Array REF.F DIM3 e0 -> GetTP (Array REF.F DIM3 e0) 2
In the first argument of ‘(.)’, namely ‘tp2’
In the second argument of ‘as’, namely ‘(tp2 . tp0)’
どうもArrayのようなデータ族ではその型パラメータに未解決の型があると閉じた型族のマッチングがうまくいかないみたいです。（データ族ではない場合や、型パラメータがe0とかでなくIntとか明確になっている場合は上手くいく模様）仕方ないので型族使わず関数を総当たりで作って対応しました（遠い目）。つまり型パラメータがn個の場合のm番目の型パラメータを取得するという関数を沢山作って対応する訳ですね。tp2_3みたいな。超ウケますね。
drawImage = do
image <- readImage "hoge.raw" 100 100 1 `as` (tp2_3.tp0) $ (0 :: Word8)
draw image
一応作ったコードはこちらに上げてます。ゴミが色々入ってますが、指差して笑うと健康にいいですよ。そしてエレガントな方法教えてください orz。僕ぁもぅ疲れた。
7/9 追記
RepaのArrayはデータ族なのですが、評価後は型引数２つしか持ってない上、型引数の順番が変わるみたいです(Data.Array.Repa.Repr.Unboxed.R:ArrayUsha a DIM3 みたいになります)。怖い。
ghci上で型を取り出せるところまではできました。
:kind! (V.Storable a) => GetTP (GetTP (IO (Array REF.F DIM3 a)) 0) 0
(V.Storable a) => GetTP (GetTP (IO (Array REF.F DIM3 a)) 0) 0 :: *
= forall a. V.Storable a => a
が、エラーメッセージは変わらず・・・ うーん
Couldn't match type ‘GetTP (Array REF.F DIM3 e0) 0’ with ‘Word16’
The type variable ‘e0’ is ambiguous
Expected type: Array REF.F DIM3 e0 -> Word16
Actual type: Array REF.F DIM3 e0 -> GetTP (Array REF.F DIM3 e0) 0
In the first argument of ‘(.)’, namely ‘tp0’
In the second argument of ‘as’, namely ‘(tp0 . tp0)’
実装についてのアレコレ
これだけだと「あ、さいですか」になるので、多少型族について小技（という程のものでもないですが）を公開しておきます。GHC拡張が沢山必要になります。私が使ったのは以下のものです。
{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, TypeFamilies #-}
{-# LANGUAGE UndecidableInstances, FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies, RankNTypes #-}
m番目の型パラメータを抜き出す型族
まずは簡単なものからいきましょう。n(<4)個の型パラメータを受け取る型のm(<n, 0スタート)番目の型、という型族はどのように作れば良いでしょうか？これはclosedな型族とやらを使うとできました。最初の型の引数に抜き出す対象となるデータ型を、次に何番目の型パラメータかを指定します。
type family GetTP (a :: *) (idx :: Nat) :: * where
GetTP (f a b c) 0 = a
GetTP (f a b) 0 = a
GetTP (f a) 0 = a
GetTP (f a b c) 1 = b
略
もちろん 前述のデータ族の話以外にも、f が曖昧だとマッチングできなくて失敗します。(f = f' a かもしれないから？)
> :kind! forall a. GetTP (Maybe a) 0
forall a. GetTP (Maybe a) 0 :: *
= forall a. a
> :kind! forall a. GetTP (Array U DIM3 a) 0
関数の戻り値の型を求める型族
haskellだとa -> b -> cとa -> (b -> c) の区別がなくて、どこまでが引数でどこからが戻り値なのかユーザーが決める必要があるのですが、面倒なので前者で解釈します。とはいえ、これもcが曖昧だと上手くいきません。（c = c' -> d'かもしれないから？） これは以降全てに言えます。つまりほとんど役に立ちません。
-- RetT (a -> b -> c) = c
type family RetT (f :: *) :: * where
RetT (a -> b) = RetT b
RetT a = a
引数の個数を型レベルで求める型族
以下のようにすればできました。型レベルで再帰的に加算するだけです。TypeLits便利ですね。
-- NumArg (a -> b -> c) = 2
type family NumArg (f :: *) :: Nat where
NumArg a = NumArg' a 0
type family NumArg' (f :: *) (offset :: Nat) :: Nat where
NumArg' (a -> b) offset = NumArg' b (offset + 1)
NumArg' a offset = offset
m番目の引数の型を抜き出す型族
こちらは少し難しくて、引数の数を予め指定する必要がありました（最初の定義の２番目の定義がオーバーラップする為？）。
-- ArgT (a -> b -> c) 1= b
type family ArgT (a :: *) (idx :: Nat) (len :: Nat) :: * where
ArgT a 0 0 = a
ArgT (a -> b) 0 len = a
ArgT (a -> b) idx len = ArgT b (idx - 1) (len - 1)
曖昧な型でも対応したい場合は抽出関数を沢山用意するとか
headT :: (a -> b) -> a
headT = undefined
tailT :: (a -> b) -> b
tailT = undefined
みたいなの作って合成して頑張るという手もあるかもしれません。
おわりに
はっきりいって今回作ったものは役に立たない上規則とか推論の仕組みを知らずにテキトーにやって今のところなんか動いてるレベルの品質です。もっと良い方法とかこれ勉強しろみたいなアドバイスがあれば是非頂けると嬉しいです。
独り言
型レベルでgetter作ったし、setterも作れるし、じゃあ型レベルのlens作れるんだろうか？機能を限定すればできそうな気がしますね。何が嬉しいかは分かりませんが。