11
8

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 5 years have passed since last update.

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

Last updated at Posted at 2017-01-26

 存在型は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多相というのは、つまりは通常の多相です。
具体的には

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期を見ながら書かれたぷりっ。
ぷしゅ〜〜。

11
8
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
11
8

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?