HaskellのRank2Typesがだいぶわかるやつ

  • 10
    いいね
  • 0
    コメント

 存在型はheterogeneousリストなどの例がわかりやすいですけど、Rank2Types (or RankNTypes) はなかなかわかりやすい例がない気がしますー。
今回、存在型とRank2Typesを使って、いい感じなコード例を作ったので報告いたします :)

仮定する知識

  1. 存在型 (ExistentialQuantification)
  2. IsString (OverloadedStrings)
    • 文字列リテラルをText型やByteString型として (IsString a => a型として) 扱えるようになるやつ
    • 具体的にはs = "ahoge" :: IsString a => aが有効なコードになる

ここでわかる知識

  1. 2ランク多相 (Rank2Types)
    • が用いられた事例のうち一つがわかる

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE Rank2Types #-}

import Data.String (IsString)
import Data.Text (Text)
import Shelly (run_)
import System.EasyFile (doesFileExist)

type FilePath' = forall s. IsString s => s

flagFile :: FilePath'
flagFile = "/tmp/flag"

-- ここに、shellyを使ったほうがいい事情があるとします。
-- 故にshelly使います (※)
createFlagFile :: IO ()
createFlagFile = shelly $ run_ "rm" ["-f", flagFile]

flagFileExists :: IO Bool
flagFileExists = doesFileExist flagFile
  • ※ 実際は「xmonadでシェルスクリプトライクなことしたかったけど、spawnだと型付けできなかったりした」というあれがあった
  • 問題は、期待する文字列型の不一致
    • run_ :: FilePath -> [Text] -> Sh ()
      • [Text]
    • doesFileExist :: FilePath -> IO Bool
      • FilePath
      • FilePath = String

解説

 ここで存在型とRank2多相を同時に用いた

type FilePath' = forall s. IsStrings s => s

という型があって、
これはExistentialQuantificationが無いと そもそも構文的に許されませんし(右辺にforallがある)
Rank2Typesが無いと この深さのforallは許されないぷりっ!

深さ

 Rank2というのはforallの深さが2であるということらしいです!
(この時点で、2ランク多相が一般化された、Nランク多相(RankNTypes)のことについてわかっていない)

 ランク1多相というのは、つまりは通常の多相です。
具体的には
haskell
f :: a -> a

これなの。

しかしこれは、こちらで示されている通り

g :: (a -> a) -> (Bool, Char)
g f = (f True, f 'a')

このfがランク1多相なので
f :: a -> a が
f :: Bool -> Bool なのか
f :: Char -> Char なのか
が決定できないぷり。 ぷりぃ……。

ここでランク2多相にすること

g :: (forall a. a -> a) -> (Bool, Char)
g f = (f True, f 'a')

によって、解決されます!

解決

 という理由により「TextでもStringでもある型のシノニム」として

type FilePath' = forall s. IsString s => s

を導入し

flagFile :: FilePath'
flagFile = "/tmp/flag"

-- 1
createFlagFile :: IO ()
createFlagFile = shelly $ run_ "rm" ["-f", flagFile]

-- 2
flagFileExists :: IO Bool
flagFileExists = doesFileExist flagFile

このような2つの決定をすることができました! ということなの!

かしこまっ!

終わり

この記事は、プリパラ2期を見ながら書かれたぷりっ。
ぷしゅ〜〜。