日々の流転

λ. 長さ付きリストに対する型安全な filter 関数

型レベルプログラミングの会(ヒビルテ(2009-04-18))の会場で出てた話だけど、(a → Bool) → Vec a n → (∃m≦n. Vec a m) みたいなやつなら定義可能。

{-# LANGUAGE EmptyDataDecls, GADTs,
  FlexibleInstances, MultiParamTypeClasses, IncoherentInstances #-}

data Z
data S n

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

class LE a b

-- one definition of ordering
instance LE Z n
instance LE n m => LE (S n) (S m)

-- another definition of ordering
instance LE n n
instance LE n m => LE n (S m)

data BoundedVec a n where
    Bounded :: LE m n => !(Vec a m) -> BoundedVec a n

vfilter :: (a -> Bool) -> Vec a n -> BoundedVec a n
vfilter f xs =
    case xs of
      VNil -> Bounded VNil
      VCons x xs ->
          case vfilter f xs of
            Bounded ys ->
              if f x
              then Bounded (VCons x ys)
              else Bounded ys

ただ、Haskellの型クラスだと推論を制御するのが難しくて、オーバーラップしたインスタンス定義(IncoherentInstances)が必要になってしまった*1。 オーバーラップしたインスタンス定義を使わない定義は型ハッカーの諸氏への課題ということで。