ランタイムのチェックを一度で済ます

http://d.hatena.ne.jp/Lost_dog/20111128/1322504143
reify_integer がおもしろいなーと思った．

これと同じ雰囲気で， dependent type の例によく出てくる「長さ n のベクトル型 Vec n a」についてこんなのが書けそう．
同じ長さ n のベクトル同士だけ zipWith．長さが異なるベクトル同士だと型が合わずにコンパイルエラー．長さが等しいことは sameLength でランタイムにチェックすることができて，一度チェックすればそれ以降は型で保証される．

{-# LANGUAGE Rank2Types, GADTs, EmptyDataDecls #-}
import Prelude hiding (zipWith, foldl)
import Control.Applicative ((<$>))

data Z
data S n

data Vec n a where
  Nil :: Vec Z a
  (:::) :: a -> Vec n a -> Vec (S n) a

toList :: Vec n a -> [a]
toList Nil = []
toList (x ::: xs) = x : toList xs

fromList :: [a] -> (forall n. Vec n a -> b) -> b
fromList [] k = k Nil
fromList (x:xs) k = fromList xs $ \ys -> k (x ::: ys)

sameLength :: Vec n a -> Vec m b -> Maybe (Vec n b)
sameLength Nil Nil = Just Nil
sameLength (_ ::: xs) (y ::: ys) = (y :::) <$> sameLength xs ys
sameLength _ _ = Nothing

zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith _ Nil Nil = Nil
zipWith f (x ::: xs) (y ::: ys) = f x y ::: zipWith f xs ys
zipWith _ _ _ = error "should not happen!"

foldl :: (a -> b -> a) -> a -> Vec n b -> a
foldl _ z Nil = z
foldl f z (x ::: xs) = foldl f (f z x) xs

innerProd :: Num a => Vec n a -> Vec n a -> a
innerProd xs ys = foldl (+) 0 $ zipWith (*) xs ys

main :: IO ()
main = do
  as <- readLn :: IO [Int]
  bs <- readLn :: IO [Int]
  fromList as $ \xs -> fromList bs $ \ys ->
    -- ここで zipWith (,) xs ys とは書けない
    case sameLength xs ys of
      Just ys' -> do
        putStr "zip: " >> print (toList $ zipWith (,) xs ys')
        putStr "innerProd: " >> print (innerProd xs ys')
      Nothing -> putStrLn $ "different length..."

実行例

% ./Vec
[1,2,3]
[4,5,6]
zip: [(1,4),(2,5),(3,6)]
innerProd: 32
% ./Vec
[1,2]
[3,4,5]
different length...