Haskell GADTで存在型から型を復元

Haskell

GADTは証拠みたいなもの(というか証明)なので この証拠さえあれば 型を存在限量で隠蔽しても パターンマッチングで復元できてしまうのであった。

コード

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}

-- 証拠
data Wit :: * -> * where
  IntWit :: Wit Int -- Int型である
  BoolWit :: Wit Bool -- Bool型である
  StringWit :: Wit String -- String型である
  ShowWit :: Show a => Wit a -- Showクラスに属する何かである…！

-- 証拠つきの存在型
data Ex = forall a. Ex (Wit a) a

-- 適当なデータ型 (Showクラスに属する)
data MyData = MyData deriving Show


heterolist :: [Ex]
heterolist = [Ex IntWit 1, Ex BoolWit True, Ex StringWit "abc", Ex ShowWit MyData]

--  GADTが証拠として機能するため, 個々の型のshowが使える
instance Show Ex where
  show (Ex IntWit i)      = show i ++ "::Int"
  show (Ex BoolWit b)     = show b ++ "::Bool"
  show (Ex StringWit str) = show str ++ "::String"
  show (Ex ShowWit a)     = show a ++"::Show a=>a"

テスト

*Main> heterolist
[1::Int,True::Bool,"abc"::String,MyData::Show a=>a]

rants

こーゆーのは Coqでは普通にinductive predicateとかで使うけど、Haskellの型クラスと組み合わせることができて驚き。

もういっちょ

こういうのは良いかも

-- import Data.Maybe (mapMaybe)
fromInt (Ex IntWit i) = Just i
fromInt _             = Nothing

extractInt = mapMaybe fromInt

ここで mapMaybe :: (a -> Maybe b) -> [a] -> [b]

*Main> :t fromInt
fromInt :: Ex -> Maybe Int

*Main> :t extractInt
extractInt :: [Ex] -> [Int]

*Main> extractInt heterolist
[1]

あとはfromInt的な関数をいちいち定義せずに済めばよいのだけど。パターンマッチが失敗したらNothingを返すのはdo記法だけ？