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

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


まとめ

  • rootなしでNixをインストールした。
  • nixを触るときはその都度prootする必要がある。

参考文献

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

型レベルリテラルと行列

行列(matrix)同士の和・差・積は、 行列の形によっては定義されない。せっかくHaskellのように強い型システムをもつ言語を採用していても、実行時エラーの潜在的原因になってしまう。

これをコンパイル時に防ぐには、行列の形まで含めて静的に型付けする。 たとえば行列の積は

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

のように定義できる。 すると、行列の形が正しいかどうかがコンパイル時に自動でチェックされる。

コンパイル時にチェックすることで受けられる恩恵は2つある。 1つは実行時エラーの潜在的原因を減らすことでプログラムの信頼性が高まることだ。これは同時に実装者の心理的負担を減らすことでもある。 もう1つは、形のチェックを前もって行うので、(ノーリスクで!)ランタイムオーバーヘッドを低減できることだ。 GHCではこのような仕組みが 型レベルリテラル によってサポートされている1

Haskell数値計算デファクトスタンダードhmatrixでは、 形の分かる行列の型L m nと形の分からない行列の型Matrix Doubleの二種類を用意し、 2つを区別している。 使う側としてはこれら区別された型どうしを行き来する必要があるのだが、 特に形の分からないものを分かるものにキャストする手段が要になる。 例として、行列を2つ読み込んで「安全な」演算を行い、最小二乗解を出力するプログラムを示す:

main = do
  x <- loadMatrix "sample1.mat" -- x :: Matrix Double
  y <- loadMatrix "sample2.mat" -- y :: Matrix Double
  let beta = withMatrix x $ \x -> -- x :: L m n
             withMatrix y $ (. exactDims) $ \case
               Nothing -> error "y has incompatible dimensions"
               Just y  -> let -- y :: L m k
                 lse = (tr x <> x) <\> tr x <> y -- lse :: L n k
                 in unwrap lse
  putStrLn "least square-error solution is:"
  print beta

このようにすると、少なくとも形の分かる部分での不整合をコンパイル時に検知できるため、 プログラマアルゴリズムの主要ロジックを安全に構築することが出来る(例えば、tr x <> xx <> xと書くとコンパイルが通らない)。 また同時に、煩雑なエラーハンドリングを最初のキャスト時に限定することが出来る(今回で言えばNothing ->のところ)。

参考


  1. 一般に型レベルリテラルが整合するどうかをコンパイル時に完全自動で判定する問題は、入力の多項式時間(現実的な時間)では解けないと考えられている。したがって、複雑なプログラムの場合にはコンパイラのチェックを人手でサポートし、半自動でチェックする必要が出てくる。

Haskell学習記(1)

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

続きを読む