pythonでcurryワンライナー

pythonを書いていて、急にcurry化したくなったときはこうする:

import functools
curry = lambda n: lambda f: lambda x: (curry(n - 1)(functools.partial(f, x)) if n > 1 else f(x))

そんでもってこう:

@curry(3)
def func(x, y, z):
    return x + y * z

print(func(42)(4)(-5))  # -> 22

Injective Functional Dependency

マルチパラメタクラスの型変数間に一対一の対応関係をもたせたいとする。 このとき、型変数の間に相互にfuncitonal dependency をもたせればよい。

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}

-- | this typechecks
class Foo a b | a -> b, b -> a where
  foo :: a
  bar :: b

Haskellの太いほうの矢印について

Haskellには頻出する矢印が2つある(->=>)。 なかでも=>(型制約導入子?)がくせものである。

  • くせものポイント1:数学の「ならば」とは(一見)違う意味を持つ。
  • くせものポイント2:もちろん日本語の「ならば」とも違う意味を持つ。
  • くせものポイント3:Haskellの中でも型クラス宣言と型インスタンス宣言で意味が違う。
  • くせものポイント4:関数宣言の引数側の制約となるか返り値側の制約となるかでも意味が違う。

というわけで、=>の使いかたを今一度整理しよう。

1. 型クラス宣言の=>

class Functor a => Applicative a where ..

意味:Applicative aならばFunctor a(逆方向)である。

2. 型インスタンス宣言の=>

instance (Foldable f, Monoid m) => Summable (f m) where ..

意味:Foldable fかつMonoid mならばSummable (f m)(順方向)である。

3. 関数宣言の=>

引数側に制約がある場合:

shinyArgFunc :: Sparkling a => a -> Int

意味:shinyArgFuncは「Sparklingインスタンス」からIntへの写像である。

返り値側に制約がある場合:

shinyReturnFunc :: Sparkling a => Int -> a

意味:shinyReturnFuncIntから「Sparklingインスタンス」への写像である。

両方に同じ型変数がある場合:

truelyShinyFunc :: Sparkling a => a -> a

意味:truelyShinyFuncは「Sparklingインスタンス」から「Sparklingインスタンス」への写像である。つまり、引数側の規則が優先される。

4. 無制約の型制約について

型制約を入れずに型変数を登場させることは、 無制約の型クラスを導入することと等価である。 従って、上のルール1-3に注意すると、無制約の型変数xから自明な実装が導かれる:

-- とあるクラスの..
class Trivial a where
  trivialThing :: a

-- 自明な無制約インスタンス
instance Trivial x where
  trivialThing = undefined

-- 自明な無制約値
trivialValue :: x
trivialValue = undefined

全ての型に共通する要素がundefinedしか無いことから、 これらの実装はundefined以外にありえない。 このへん、インスタンス宣言における型制約導入と関数の返り値における型制約導入の類似性が滲み出ている。

5. まとめ

  • 型クラス宣言と型インスタンス宣言における型制約は集合論的には意味が逆*1
  • 関数宣言における型制約も場所によって意味が逆転する。
  • 無制約の型制約による対比から、型クラス↔引数、型インスタンス↔返り値の対応が取れる。

*1:この場合の型制約導入子はインスタンスの実装順を表すとも取れる。そう考えると意味は一緒。

Nixパッケージマネージャとproot

背景

  • Nixはバージョン管理に強いパッケージマネージャーのひとつ。同じライブラリの異なるバージョンを共存させたり、環境設定を巻き戻したりすることが得意。
  • 今回は「Nixを使いたいがrootがないので/nixを作成できない」場合に対処する方法についてまとめる。

方法

PRootのセットアップ

tallocライブラリが必要なのでインストールしておく。たとえばLinuxbrewなどから。

cd $workingdir
git clone https://github.com/proot-me/PRoot.git
cd PRoot/src
make
cp proot $binpath 

簡単ですね。

Nixのインストール

/nixの代わりとなるディレクトリを用意してprootでマウント

mkdir $hostdir  # 例えば~/nix-mntなど
proot -b $hostdir:$/nix bash # お好みのシェルでどうぞ

続けてprootシェル内でNixをインストール

curl https://nixos.org/nix/install | sh

以上。私はfishシェルを使っていたので、さらにマウント直後に

fenv source $HOME/.nix-profile/etc/profile.d/nix.sh

を実行するように設定した。


まとめ

  • PRootでNixをユーザーランドにインストールした。
  • nixを触るときはその都度prootする必要がある。

参考文献

https://nixos.org/wiki/How_to_install_nix_in_home_(on_another_distribution)#Building_native_packages

副作用の閉じ込めテクニック

前説

Haskell純粋関数はよいものだ。 自然とコードのモジュラリティを高めてくれるおかげで再利用し易いコードが出来上がるし、 時には自分でも気づかなかった、本当に書きたかった実装を教えてくれさえする。 また副作用を許容しないということはある変数の値の構築に関わったプロセスを明確にするということなので、 デバッグの過程をとても簡単にしてくれる。

一方で、プログラムに状態はつきものだ。 例えばインタラクティブなソフトウェアや、データ構造に依存するアルゴリズムは常に状態とともにあるし、 そもそも普段使われる計算機は全て、内部状態を変化させることで計算を行う。 つまりソフトウェア/ハードウェアの各レベルにおいて、 状態をうまく扱う方法はプログラミングの重要な技術となる。 そんなわけで、今回は純粋関数を用いて状態とうまく付き合っていく方法について整理する。


動機

状態をともなう計算の純粋な表現は、特に複合的な場合に難しい。 例を見てみよう。 まず単純な状態計算は次のように表現される:

function :: Input -> State -> (Output, State)

返り値に出力だけでなく計算後の状態が含まれていることに注意したい。 この型の計算を反復する場合、例えばこうなる:

repetive :: [Input] -> State -> ([Output], State)
repetive [] state0 = ([], state0)
repetive (x:xs) state0 = (y:ys, stateLast) where
  (y, state1) = function x state0
  (ys, stateLast) = repetive xs state1

本質的には、状態を引き回しながら各入力にfunctionを適用しているだけなのだが、 計算過程の状態と入出力の変数が混在しているため、計算の流れが見えにくくなっていることがわかるだろう。 この例では、状態の計算の流れ(fold)と入出力の計算の流れ(map)が混ざっていることがわかりにくさの原因のような気がする。

では、この実装を隠蔽する高階関数を作ってみよう。 状態に対してfoldし、入力に対してmapする高階関数は次のように書かれる:

mapS :: (input -> state -> (output, state)) -> [input] -> state -> ([output], state)
mapS f [] state0 = ([], state0)
mapS f (x:xs) state0 = (y:ys, stateLast) where
  (y, state1) = f x state0
  (ys, stateLast) = mapS f xs state1

これを用いれば、先の関数はrepetive = mapS functionと書くことが出来て、 関数repetiveの実態が「状態を伴いつつ関数functionmapするもの」であることがわかりやすくなる。 めでたい。

さて、状態の計算ほど普遍的な計算となれば使いまわすことも増えるし、 他人に公開するソースコード中に登場させることもあるかもしれない。 そんなとき、mapSのような実装の読みくいオレオレ関数ではなくて、 共通の枠組みを用いて簡潔に記述したくなってくる。 ここで役に立つのがStateモナドである。


Stateモナド

モナドの記法を利用することで、状態を明記する煩わしさから解放される。 Stateモナド風に書けば、ちょうどmapSmapMに対応する:

import Control.Monad.Trans.State.Lazy (runState, state)

mapS = (runState =<<) . mapM . (state =<<)

ごちゃごちゃしていたmapSの実装がたった一行に。うれしい。

一方、そもそも状態の計算を関数的に書くことそのものが、可読性の意味で劣るということもあり得る。 そんなときにはmapMの変種forMを使うと、状態操作の部分をキレイに露出できる:

import Control.Monad (forM)

repetive xs = runState . forM xs $ \x -> state (function x)

最後のfunction xの部分をさらに細かく書き下せば、 foreach式の表現で状態計算を記述できることがわかるだろう。


具体例

抽象的な話ばかりではスッキリしないので、具体例を示しておく。 以下は辞書(Counter型)から連続で要素を取り出す例。 まずは再帰を使ったナイーブな実装:

import qualified Data.Map.Strict as Map
type Counter = Map.Map String Int

seqpop1 :: [String] -> Counter -> ([Maybe Int], Counter)
seqpop1 [] dict = dict
seqpop1 (key:ks) dict = (value:vs, dictLast) where
  value = Map.lookup key dict
  dict' = Map.delete key dict
  (vs, dictLast) = popByList1 ks dict'

二分木から連続で値を取り出すだけにしては記述が冗長すぎる。

次に高階関数を用いた抽象化:

seqpop2 :: [String] -> Counter -> ([Maybe Int], Counter)
seqpop2 = mapS pop where
  pop key dict = (Map.lookup key dict, Map.delete key dict) -- lookupとdeleteを状態計算の正準型にまとめる

だいぶ良くなった。何をしたいのかはすぐ読めるし、記述量が減っている。 しかしmapSの実装を読まないことにはこの関数の正確な動作がわからないし、 もっと複雑な計算ではmapSの第一引数がもっさりするかもしれない。

最後にStateモナドを用いる実装を2種:

import Control.Monad.Trans.State.Lazy (runState, state, get, modify')


seqpop3 :: [String] -> Counter -> ([Maybe Int], Counter)
seqpop3 keys = runState $ mapM pop' keys where
  pop' key = do
    value <- Map.lookup key =<< get
    modify' (Map.delete key)
    return value


seqpop4 :: [String] -> Counter -> ([Maybe Int], Counter)
seqpop4 keys dict = (`runState` dict) $
  forM keys $ \key -> do
    value <- Map.lookup key =<< get
    modify' (Map.delete key)
    return value

mapMバージョン、forMバージョンともに、 最初の再帰の例なみに記述量が多いが、 状態と値の流れがもっともわかりやすい。


まとめ

状態をともなう計算のわかりやすさと純粋さを両立する方法について、整理してみた。 特に、状態計算を高階関数として隠蔽する方法と、モナドを利用して簡潔に書く方法についてまとめた。

型レベルリテラルと行列

行列(matrix)同士の和・差・積は、 行列の形によって定義されたりされなかったりするため、科学技術計算において予期しない実行時エラーの原因になることがある。 これをコンパイル時に防ぐには、行列の形まで含めて静的に型付けすればよい。 たとえば行列の積を

matmul :: Matrix a b -> Matrix b c -> Matrix a c

のように定義すれば、 matmulは行列の形が原因では実行時エラーとならないことが コンパイル時の型チェックによって保証される。 Haskellではこのような仕組みが 型レベルリテラル によってサポートされており、DataKinds言語拡張を通して使用可能になる。

ところがこの仕組みも万能ではない。 問題は、多くの場合行列の形(aとかbとかcとか)はコンパイル時点で未知数ということだ。 例えば統計処理プログラムでは、入力データの総数が実行時に初めて分かったりする。 なぜこれが問題かというと、一般に未知の型レベルリテラルが整合するどうかをコンパイル時に判定する問題は 「定理の自動証明」と同等に困難(絶対に解けないケースが存在する)なのだ。

ではどうするか。 hmatrixライブラリによる行列演算の実装では、 形の分かる行列の型L m nと形の分からない行列の型Matrix ℝの二種類を用意し、 2つを区別している。 使う側としてはこれら区別された型どうしを行き来する必要があるのだが、 特に形の分からないものを分かるものにキャストする手段が要になる:

withMatrix :: forall z . Matrix ℝ -> (forall m n . (KnownNat m, KnownNat n) => L m n -> z) -> z

当然「形の分からない行列のクラス」より「形の分かる行列のクラス」のほうが小さいため、 この関数は安全ではない。 つまり、実行時エラーを防ぐことができない。 ではこの「区別」にどのようなご利益があるかというと、 少なくとも「形の分かる部分」での不整合をコンパイル時に検知できるため、 アルゴリズムの主要部を安全に構築することが出来るということだ。 逆に言えば、実行時エラーを形の分からない部分のみに限定することが出来る。 しかも、冒頭の例で上げたように 多相な型レベルリテラル(aとかbとかcとか)を利用することで Haskell型推論の力を借りて整合性をチェックすることが出来るので、 チェック可能な範囲はそこそこ広い。

参考

Haskell学習記(1)

少し前にHaskellの勉強を始めて軌道に乗りだしたので、初志を忘れないように、ポストLYHGGの歩みを書き留めておく。

続きを読む