GHC の演算子の優先順位には -1 がある（たぶん組込でしか使えない #Haskell pic.twitter.com/Xa0OIjvw5i
— o̞͑kä̝mo̞͑to̞͑ kä̝zʊ̠kɪ̟ (@kakkun61) January 3, 2021
Case Analysis 関数
今回は case analysis と呼ばれる関数の話です1。
data D a b c = C0 a b | C1 c
例えば上記のようなデータ型があった場合 case analysis 関数は次のようになります。
d :: (a -> b -> d) -> (c -> d) -> D a b c -> d d f _ (C0 a b) = f a b d _ f (C1 c) = f c
値構築子の数だけ関数を引数とし、対象のデータを最後の引数とします。それぞれの関数の型は値構築子の型に似ます。
C0 :: a -> b -> D a b c C1 :: c -> D a b c d :: (a -> b -> d) -> -- C0 の型から決まる (c -> d) -> -- C1 の型から決まる D a b c -> -- 対象のデータ型 d
使い方としては case 式でのパターンマッチの代わりにワンライナーとして使うことが多いです。次の2つのコードは等価です。
case v of C0 a b -> f a b C1 c -> g c
d f g v
base にある case analysis 関数としては次のようなものがあります。
Data.Bool.bool :: a -> a -> Bool -> a Data.Maybe.maybe :: b -> (a -> b) -> Maybe a -> b Data.Either.either :: (a -> c) -> (b -> c) -> Either a b -> c Data.List.foldr :: (a -> b -> b) -> b -> [a] -> b -- 実際は多態、構築子と引数の順番が反対
-
case analysis の名前は
boolやeitherのドキュメントで使われています。eliminator 派もあるようです。↩
続・刹那的純粋関数的データ構造と線形型
The English version is at Dev.
前回の記事の追加情報です。
pure 抜け道はなかった
まあ、こういうインターフェースでありがちな
pureで外に出す抜け道が存在するのですが。
最後にこういうことを無思慮に書いたわけですが、Dev に書いた英語版を Reddit に載せたところ有益な情報を教えてもらえました。
I think the solution to the problem with
emptymight be to use theUr(for "unrestricted") datatype from linear-base:
empty :: (Queue a #-> Ur b) #-> Ur bTrying to run
empty Urshouldn't typecheck, because theUrconstructor is not linear. This seems to be an idiom used in other places of linear-base.
継続の返り値を Ur にすることで Queue を外に出せなくなります。Ur :: a -> Ur a に渡すと何回も使われるかもしれないため1回しか使えない Queue は渡すことができません。なるほどー。
CPS にしなくてよかった
生成する関数（ここでは empty）以外は CPS にしなくていいことに気付きました。
線形関数の中でその引数に別の線形関数を適用するとその返り値にも線形性が付くようです。この辺りちゃんと型付け規則を確認しないとな。
idl の返り値の a も1回しか使えないという性質を引き継いでるんだな。まあそうじゃないと困るが。 pic.twitter.com/PoZCkWkO5e
— o̞͑kä̝mo̞͑to̞͑ kä̝zʊ̠kɪ̟ (@kakkun61) December 21, 2020
つまり、empty の継続 Queue a #-> Ur b の中で enqueue などを呼ぶとその返り値も1回しか使えないわけなので、enqueue などは CPS にしなくてよかったです。逆に null の Bool は何回使ってもいいので Ur でくるみます。
null :: Queue a #-> (Ur Bool, Queue a) null (Queue l m) = (Ur (P.null l), Queue l m) enqueue :: a -> Queue a #-> Queue a enqueue a (Queue l m) = check l (a:m) dequeue :: Queue a #-> (Ur (Maybe a), Queue a) dequeue (Queue (a:l) m) = (Ur (Just a), check l m) dequeue (Queue l m) = (Ur Nothing, Queue l m)
そんなわけで使用感としてはこんな感じになりました。let 式が使えるなら見やすいのですが。
it "empty → enqueue → dequeue" $ do let f :: Queue Int #-> Ur Int f q = enqueue 0 q PL.& \q -> dequeue q PL.& \(Ur (Just a), q) -> q `lseq` Ur a Ur a = empty f a `shouldBe` 0
刹那的純粋関数的データ構造と線形型
The English version is at Dev.
『純粋関数型データ構造』（以降 PFDS）の5.2章に刹那的純粋関数的キューというものが出てきます。
asciidwango.jpこのキューは計算量の関係から1つの値に対して1回しか操作をしてはいけません。例えば下記操作列なら大丈夫ですが、その次の操作列では計算量が大きくなる可能性があります。
-- よい例 ops = let q0 = empty q1 = enqueue 0 q0 q2 = enqueue 1 q1 Just (a, _) = dequeue q2 in a
-- ダメな例 ops = let q0 = empty q1 = enqueue 0 q0 q2 = enqueue 1 q1 q2' = enqueue 2 q1 -- q1 を2回使っている Just (a, _) = dequeue q2 Just (b, _) = dequeue q2' in (a, b)
この1回しか操作してはいけないという性質を線形型で守れないか、というのがこの記事の主題です。
GHC の線形型については前回の記事を参考にしてください。
実装
GHC での線形型は線形関数（linear arrow）1として実装されているため、操作は継続渡しスタイルで実装していきます。例えば empty は下記のような型になります。
empty :: (Queue a #-> b) #-> b
継続の型が Queue a #-> b となっているのでこの関数の中では引数の Queue a 型の値は1回しか使えません。型検査器が検査してくれます。
そんなこんなで実装すると下記のようになります。計算量については PFDS を参照してください。
{-# LANGUAGE GADTs #-} {-# LANGUAGE LinearTypes #-} {-# LANGUAGE Strict #-} data Queue a where Queue :: [a] -> [a] -> Queue a deriving (Show) empty :: (Queue a #-> b) #-> b empty f = f (Queue [] []) null :: Queue a #-> Bool null (Queue l _) = Prelude.null l enqueue :: a -> Queue a #-> (Queue a #-> b) #-> b enqueue a (Queue l m) f = f (check l (a:m)) dequeue :: Queue a #-> (Maybe (a, Queue a) #-> b) #-> b dequeue (Queue (a:l) m) f = f (Just (a, check l m)) dequeue (Queue _ _) f = f Nothing check :: [a] -> [a] -> Queue a check [] m = Queue (reverse m) [] check l m = Queue l m
Queue を GADT を使って実装しているのは null のような関数を実装するためで GADT を使わなければ Queue l m の l や m も再帰的に「1回使う」という制約（線形性）が付くため _ でマッチすることができません。線形型版の null があったとして null l && null m と書けたとしてもリストに対しても再帰的に線形性を求められるため結局リストの構造を全部たどることになります。
ただ、この実装だと困ったことがあって、線形型では1回は使わないといけないため Queue a の値を消すことができません。返り値にしないといけなくなります。そこで前回の記事にも出てきた Consumable 型クラスの consume で消費できるようにインスタンスにします。
instance Consumable a => Consumable (Queue a) where consume (Queue l m) = l `lseq` m `lseq` ()
さてこれで使えるようになりました。
> import Prelude.Linear (lseq) > import Data.Queue.Ephemeral > empty (\q0 -> enqueue 0 q0 (\q1 -> dequeue q1 (\(Just (a, q2)) -> q2 `lseq` a))) :: Int 0
……いや、確かに使えるか使えないかで言ったら使えますが、使いやすいか使いにくいかで言ったら使いにくいですね？
継続モナド
継続渡しスタイルならモナドにすることができるため do 記法を使って読みやすくすることができます。
さて線形型版でもできるのでしょうか？やってみましょう。……（3日が経過）できました！全文はリポジトリーを見ていただくとして下記の型を線形型版モナドのインスタンスにすることができました。線形型に慣れていなかったため型合わせが想像以上に大変でした。
newtype ContT r m a = ContT { runContT :: (a #-> m r) #-> m r }
使ってみましょう。
> :set -XQualifiedDo > import Prelude.Linear (lseq) > import qualified Prelude.Linear as PL > import Data.Queue.Ephemeral > import Control.Monad.Trans.Cont.Linear > import qualified Control.Monad.Linear as ML > :{ | PL.flip runCont PL.id $ ML.do | q0 <- cont empty | q1 <- cont (enqueue (0 :: Int) q0) | Just (a, q2) <- cont (dequeue q1) | q2 `lseq` ML.pure a | :} 0
やったぜ。
まあ、こういうインターフェースでありがちな pure で外に出す抜け道が存在するのですが。
リポジトリー
追記（2021.01.01）
続編を書きました。 kakkun61.hatenablog.com-
ここでいう線形関数は一次関数という意味ではありません。↩
とりとめのない GHC 線形型メモ
GHC 9.0.1 alpha 1 がリリースされたときに線形型をいじってみていたことをメモしていなかったので思い出しながらメモしていく。
使用バージョン
- GHC 9.0.0.20200925
- 上記リンクのもの
ghcup ならそれ経由でインストールできる。
ghcups の場合は手動インストール後、下記のような設定ファイルで切り替えができるようになる1。
ghc: 9.0.1-alpha1: H:\programs\ghc-9.0.0.20200925-x86_64-unknown-mingw32\bin
線形型とは
GHC では引数が1回しか使えない（1回は使わないといけない）関数型として線形型が実装されている。
- 一般の関数：
- 線形型の関数：
は Haskell 文法としては
a %1 -> b として書く。
a %1 -> b は a %'One -> b の別名で（' は data kinds 拡張のシングルクォート）、a %'One -> b は FUN 'One a b の別名となっている。これにともなって a -> b は FUN 'Many a b の別名となった。FUN の型は下記のようになっている。
FUN :: Multiplicity -> forall (r1 r2 :: RuntimeRep). TYPE r1 -> TYPE r2 data Multiplicity = One -- represents 1 | Many -- represents ω
最終的には上記のようになるようだが 9.0.1 alpha 1 の時点では は
a #-> b と記述する。
a #-> b から a %1 -> b に変わった理由の1つとしては overloaded labels が将来的に型レベルに持ち上げられたときの文法の衝突を回避することがあるらしい。
マージ前だと a ->. b の時期もあったようだ。
ちょうど1回
準備ができたらコードを書いてみる。下記コマンドで REPL を起動する。
ghc --interactive -XLinearTypes
まず最初にエラーを起こしてみる。
f :: Int #-> (Int, Int) f a = (a, a)
<interactive>:3:3: error:
* Couldn't match type 'Many with 'One
arising from multiplicity of `a'
* In an equation for `f': f a = (a, a)
a が2回使用されているので推論される f の型は a -> (a, a) つまり FUN 'Many a (a, a) だが、注釈は Int #-> (Int, Int) つまり FUN 'One Int (Int, Int) なので FUN の第1引数である Multiplicity が不一致だと言っている。
引数を1回も使用しなくても同じエラーとなる。
f :: Int #-> (Int, Int) f a = (1, 2)
<interactive>:7:3: error:
* Couldn't match type 'Many with 'One
arising from multiplicity of `a'
* In an equation for `f': f a = (1, 2)
ちょうど1回使用するともちろんうまくいく。
f :: Int #-> (Int, Int) f a = (a, 1)
注釈がない場合、ちょうど1回しか使っていなくても multiplicity は （many）となる。multiplicity ポリモーフィズムは今のところない。
Prelude> g a = ((a, 1) :: (Int, Int)) Prelude> :type g g :: Int -> (Int, Int)
a #-> b を a -> b としても使えるというような部分型関係はない。
h :: Int -> (Int, Int) h = f
<interactive>:21:5: error:
* Couldn't match type 'One with 'Many
Expected: Int -> (Int, Int)
Actual: Int #-> (Int, Int)
* In the expression: f
In an equation for `h': h = f
引数を明記すると、これは妥当である。
h :: Int -> (Int, Int) h a = f a
f = g と f a = g a の意味が同じでないというのはこれまでの Haskell の感覚からすると注意が必要なところに思える。
パターンマッチをすると1回使ったとカウントされるので下記のようなコードも妥当である。
consume :: Bool #-> () consume False -> () consume True -> ()
引数に関係なく返り値が同じだからと次のように書くと、これは引数未使用となるためエラーとなる。これもうっかりまちがえそうだ。
consume :: Bool #-> () consume _ -> ()
<interactive>:1:33: error:
* Couldn't match type 'Many with 'One
arising from a non-linear pattern
* In the pattern: _
In an equation for `consume': consume _ = ()
linear-base
GHC への線形型を提案して実装した Tweag が作っている線形型対応の base パッケージが linear-base で、ここからはそれを使っていく。使用リビジョンは 341007891ae77959ac7b147f008e3a1d9c46e96b である。
multiplicity ポリモーフィズムはない
multiplicity ポリモーフィズムがないので ($) は線形版との使い分けが必要である。
f $ 1 -- error: Couldn't match type ‘'Many’ with ‘'One’ arising from an application
import qualified Prelude.Linear as L f L.$ 1
現状 case 式は線形型非対応なので case x of … と書くと x は複数回使用したとみなされてしまう。それを回避するために lambda case 拡張2を使ったイディオムが必要となる（参考）。
{-# LANGUAGE LambdaCase #-} import Prelude.Linear ((&)) maybeFlip :: Int #-> Int #-> (a,a) -> a maybeFlip i j (x,y) = i < j & \case True -> x False -> y
let や where も線形型非対応なので注意が必要である（参考）。
Consumable 型クラス
先述した consume 関数は Data.Unrestricted.Linear モジュールの Consumable 型クラスで提供されている（参考）。
class Consumable a where consume :: a #-> ()
Dupable 型クラス
最初の例で2回使えないという話をしたが、アドホックポリモーフィズムを使えば実装できる（参考）。V :: Nat -> Type -> Type は型レベル長さ付きベクトルである（参考）。
-- | The laws of @Dupable@ are dual to those of 'Monoid': -- -- * @first consume (dup2 a) ≃ a ≃ second consume (dup2 a)@ (neutrality) -- * @first dup2 (dup2 a) ≃ (second dup2 (dup2 a))@ (associativity) -- -- Where the @(≃)@ sign represents equality up to type isomorphism. -- -- When implementing 'Dupable' instances for composite types, using 'dupV' -- should be more convenient since 'V' has a zipping 'Applicative' instance. class Consumable a => Dupable a where {-# MINIMAL dupV | dup2 #-} dupV :: forall n. KnownNat n => a #-> V n a dup2 :: a #-> (a, a)
Bool に対する実装は下記になっている。ここで Data は Data.Functor.Linear.Internal である。
instance Dupable Bool where dupV True = Data.pure True dupV False = Data.pure False
pure は線形型版アプリカティブファンクターのもので下記の型を持つ。
class Functor f => Applicative f where pure :: a -> f a …
dupV の引数はパターンマッチで1回しか使っていなくて、pure に渡した True や False は何回でも使えるから pure に渡せて pure は線形関数じゃないから複製ができるということかな。
Ur 型
linear-base で1つキモになる型に Ur 型がある（参考）。
-- | @Ur a@ represents unrestricted values of type @a@ in a linear -- context. The key idea is that because the contructor holds @a@ with a -- regular arrow, a function that uses @Ur a@ linearly can use @a@ -- however it likes. -- > someLinear :: Ur a #-> (a,a) -- > someLinear (Ur a) = (a,a) data Ur a where Ur :: a -> Ur a
線形型文脈の中に何回も使える普通の値を埋め込む型で、Ur 値構築子の型が a #-> Ur a ではなく a -> Ur a となっているので中身の a 型の値は何回でも使えるようになっている。
追記（2020.12.19）
Ur の定義を下記のようにすると型構築子のカインドも値構築子の型も上記と同じとなるが線形関数と一緒に用いると型検査に違いが出る。
data Ur a = Ur a下記のような線形関数を考える。
f :: Ur a #-> (a, a) f (Ur a) = (a, a)GADT を使った定義だと問題なく型検査が通るが、後者の定義だと下記のエラーが出る。
<interactive>:40:31: error:
• Couldn't match type ‘'Many’ with ‘'One’
arising from multiplicity of ‘a’
• In the pattern: Ur a
In an equation for ‘f’: f (Ur a) = (a, a)
Movable 型クラス
線形関数の引数を Ur で包む関数をもつのが Movable 型クラスである（参考）。
-- | The laws of the @Movable@ class mean that @move@ is compatible with -- @consume@ and @dup@. -- -- * @case move x of {Ur _ -> ()} = consume x@ -- * @case move x of {Ur x -> x} = x@ -- * @case move x of {Ur x -> (x, x)} = dup2 x@ class Dupable a => Movable a where move :: a #-> Ur a
Functor・Applicative・Monad 型クラス
linear-base の提供する Functor と Applicative には2種類ある。
まず Data.Functor.Linear.Internal から見ていく。
class Functor f where fmap :: (a #-> b) -> f a #-> f b class Functor f => Applicative f where pure :: a -> f a (<*>) :: f (a #-> b) #-> f a #-> f b liftA2 :: (a #-> b #-> c) -> f a #-> f b #-> f c
もう1つは Control.Monad.Linear.Internal にある。Data は上記の Data.Functor.Linear.Internal である。
class Data.Functor f => Functor f where fmap :: (a #-> b) #-> f a #-> f b class (Data.Applicative f, Functor f) => Applicative f where pure :: a #-> f a (<*>) :: f (a #-> b) #-> f a #-> f b liftA2 :: (a #-> b #-> c) #-> f a #-> f b #-> f c class Applicative m => Monad m where (>>=) :: m a #-> (a #-> m b) #-> m b (>>) :: m () #-> m a #-> m a
前者は一部普通の関数だが後者は全部線形関数になっている。
fmap :: (a #-> b) -> f a #-> f b fmap :: (a #-> b) #-> f a #-> f b pure :: a -> f a pure :: a #-> f a liftA2 :: (a #-> b #-> c) -> f a #-> f b #-> f c liftA2 :: (a #-> b #-> c) #-> f a #-> f b #-> f c
前者だとモナドっぽいものにならないのかな（よく分かってない）。
ほか
linear-base にはまだ見るべきところがあるようだが、まだ見てないので終わり。User guide に記載の下記などは気になる。
Here's a list of new abstractions made possible by linear types:
Tweag のブログの線形型応用例。なるほどとなった。
参考
- ghc-proposals/0111-linear-types.rst at master · ghc-proposals/ghc-proposals · GitHub
- プロポーザル
- これを読まなきゃ始まらない
- GitHub - tweag/linear-base: Standard library for linear types in Haskell.
- イディオムが学びになる
- GHCの線形型プロトタイプを試すだけ - syocy’s diary
- 文法が古いが線形型とリソース管理に関する日本語記事
Windows から Windows コンテナーと Linux コンテナーの両方の Docker を使う
Docker Desktop for Windows は Windows コンテナーと Linux コンテナーが使えるのだけど排他的になっている。
そう思ってスクショを取るために切り替えボタンを押してみたら今はそうじゃない？Windows/Linux コンテナーの切り替え、前は完全に排他的だったと思ったけど、今は実行は両方できるのか？あとホストの再起動要らなくなってる？
まあ、そもそも Docker Desktop for Windows のコンテナーが排他的なの理由が分からないのよな。
で、両方のコンテナーをいじりたいのでラッパープログラムを作った。その内要らなくなりそうだけど。
イメージ図としては下図のような感じ。
Windows と WSL2 Linux のそれぞれで Docker サーバーを立てて、Windows の Docker クライアントから両方にアクセスする。docker コマンドの --host オプションを使えば接続先のサーバーを選べるので。あとは --volume のパスの変換をしてやる。
下の1行目を実行すると2行目に変換する感じ。
> kb --linux --volume C:\Users\kazuki\:/work run --rm -i hello-world > docker --host tcp://127.0.0.1:9266 run --volume /mnt/c/Users/kazuki/:/work --rm -i hello-world
> kb --help Usage: kb [OPTION...] ARGUMENTS 鯨箱 Options: -l --linux Use Linux container -w --windows Use Windows container -d DISTRIBUTION --distribution=DISTRIBUTION Select a distribution on WSL 2 -s --setup Setup Docker for Kujira Bako -V VOLUME --volume=VOLUME Mount a volume -? --help display this help and exit -v[n] --verbose[=n] set verbosity level
とりあえずラッパーにしたけど、本来なら Docker Desktop for Windows を改修するのが筋がいいよなあ。Windows コンテナー選択時はこの変換をやってるんだろうし（未確認）。
参考
無職になりました
無職になりました。
とりあえず異世界行ったら本気出しますかね。
経緯
経緯としては鬱になって休職をしていたのですが、休職できる期間が9ヶ月だったので満了しました（在職期間によって休職可能期間が変わるようです）。
これから
とりあえず失職にともなってもらえるものをもらうための手続きを忘れずにしないといけないですね。
失業のプロの方がいらっしゃればアドバイスください。あと確定申告についても。
健康保険
2年は在職中と同じ健康保険を任意継続できるので、11月14日までに申請をしないといけない。
申請用紙が送付されてくるので、それ待ち。
任意継続しないなら国民健康保険に入るらしいですが、元々ある程度の給料があれば任意継続した方がお得っぽい（よく分かってない）。
ただ、任意継続しても、以前の会社負担分も個人で負担する必要があるので倍の出費になるっぽい（ひえー）。
人の扶養に入って生活するなら、その人の被扶養者となるみたい。
失業給付
ハローワークに申請するっぽい。
申請時に離職票が必要で離職後2・3週間したら会社から送付されてくるっぽいのでそれを持ってハローワークに行くっぽい。
人事の人は受けられるっぽいことを言っていたが休養中なので受けられないんじゃないかという気もする。とりあえずハローワーク行って聞いてみよう。
「失業」とは、離職した方が、「就職しようとする意思といつでも就職できる能力があるにもかかわらず職業に就けず、積極的に求職活動を行っている状態にある」ことをいいます。したがって、次のような状態にあるときは、失業給付を受けることができません。
- 病気やけがのために、すぐには就職できないとき
あと、同人活動の収入によっては給付対象外になりそう。
本来は、基本手当を受けられないにもかかわらず、虚偽の申告などにより基本手当の支給を受けようとした場合には、不正受給としてそれ以後の支給がすべて停止され、厳しい処分が行われます（他の給付も同様です。）。
次のようなことは、絶対に行わないようにしてください。
- 内職や手伝いをした事実や収入を隠したり、偽った申告をする。
医療費控除
医療費控除のこと何も考えてなかったから今年のほとんどの領収書は捨てちゃったな。
税務署に聞きに行く。
損害保険
よく分からない封筒が届いたので会社に聞かなきゃいけない。
確定申告
確定申告もしないといけない。来年3月に前年分の申請をするんだっけ？よく分かってない。
これも税務署に聞きに行く。
そのあと
とりあえず年末年始を避けて11月中に一時帰省しようかと思っています。
ゴートゥートラベルやらうまく使えるんだろうか？
結局これもよく分かってないな。
最後に
物的支援をよろしくお願いします！前回ご支援いただいた方々ありがとうございました！
