Posted at

PureScriptで存在型を試す

More than 1 year has passed since last update.

またまたたのしい誰得記事です。PureScript知ってる人向けです。


なんでも入る箱

Haskellにはどうやら存在量化(Existential Quantification)という言語拡張があって、以下のようなことができるようです。(参考: https://ja.wikibooks.org/wiki/Haskell/存在量化された型)


Haskell

-- 右辺にforallが書ける

data ShowBox = forall s. Show s => SB s

-- Showのインスタンスにする
instance Show ShowBox where
show (SB s) = show s -- showが呼べてしまう

heteroList :: [ShowBox]
heteroList = [ SB (), SB 5, SB True ] -- 異なる型をリストにまとめる

main :: IO ()
main = mapM_ (putStrLn . show) heteroList

-- output:
-- ()
-- 5
-- True


いわゆる、データコンストラクタを関数として見たときの型制約が書けるようになるってことですかね。何に使えるかはいまいち分からないけどたのしい。


試しにこれをPureScript上で書いてみると、


PureScript

data ShowBox = forall s. Show s => SB s -- そもそも右辺にforallがかけない!コンパイルエラー!!!


言語機能自体がないようです。何でもshowできる箱はPureScriptで作ることはできないのでしょうか……


purescript-exists

言語仕様としては存在しないけど、同じ事を実現できると謳うライブラリがリリースされていました。

purescript-exists

なんですけど、れどめ見ても実際のAPIを見ても、どうやってこれを使ってShowBoxを??ってなったので色々試してみました。


できました


PureScript

-- 任意のaに対して値とshowをセットで扱う

newtype ShowBox' a = SB { value :: a, show :: a -> String }

-- aがどこかにきえた!
newtype ShowBox = ShowBox (Exists ShowBox')

instance showSB :: Show ShowBox where
show (ShowBox sb) = sb # runExists \(SB { show: sh, value }) -> sh value -- なかのshowにvalueをぶつけるだけ

-- コンストラクタのような
mkShowBox :: forall a. Show a => a -> ShowBox
mkShowBox = ShowBox <<< mkExists <<< SB <<< { value: _, show }

main :: Effect Unit
main = do
let hetero = [ mkShowBox 1, mkShowBox "abc", mkShowBox [ unit, unit ], mkShowBox { x: Just 123, y: 1000.0 } ]
traverse_ (log <<< show) hetero

-- output:
-- 1
-- "abc"
-- [unit,unit]
-- { x: (Just 123), y: 1000.0 }


できたけど……えっめんどくさい!

aの型にShowの制約を付けることはできないので、show関数と一緒にパックしてるのが肝です。


しくみ

mkExists :: forall f a. f a -> Exists f

mkExists = unsafeCoerce

unsafe!!!!!

単に型を覆い隠してまとめて扱えるようにしてるだけだった!!

でも、

runExists :: forall f r. (forall a. f a -> r) -> Exists f -> r

runExists = unsafeCoerce

こっちはちょっと面白い。

「全てのaに対して成り立つf a -> rの関数を用意して、それを経由してのみ中身を取り出せる」ということになってる。Exists fにはaの情報は一切無いけど、型に矛盾を起こさずに操作ができるわけです。かしこい。


おわり

存在量化っていう単語の意味もよく分かってないけど、イメージ的にはコンストラクタに入れられる型が和集合になってるような感じかな。どちらかというと、オブジェクト指向的な抽象化の一種な気がする。あっぷきゃすとあっぷきゃすと。

ちなみに、PureScriptの主流なUIライブラリの一つであるpurescript-halogenのなかではこれと同じ仕組みの抽象化が多用されてる。使えるシーンでは使える……ということなのだろうか。

あと、Existential Quantificationって単語、Haskellの中でもダントツに中二感たかいと思うの(どうでもいい)

全体のコード