Scala覚え書き(構文編)

最近Scalaを始めました。(函数型プログラミングと手続型プログラミングの良いとこ取りをできると聞いて)

以下覚え書きみたいな感じでこの数日で学んだことを書いていきます。
主にJavaを知っている人向けにJavaとの違いをメインに書きます。
今回は構文の話です。

構文

演算子

四則演算

Javaでは四則演算はint, long, doubleなどのプリミティブ型にしか使えませんでしたが、ScalaではBigInt(scala.math.BigInt, BigIntegerのScala版)などの型を持つ値に対しても使用可能になっています。またユーザーの定義する型についても自由に演算子を定義することが可能です。

1引数メソッドとの関係

Scalaでは四則演算を含む演算子はただの1引数のメソッドとして定義されており、例えば

a + b

という式は

a.+(b)

として解釈されます。逆に1引数のメソッドは(その名前が何であっても)中置記法の2項演算子として書くことができ、例えばBigIntのpowメソッドを呼び出す際に、

a pow 4

と書けば

a.pow(4)

と同じ扱いになります。
演算子の優先順序や結合性はその名前の最初の文字などによって決められており(例えばここを参照)、このためシフト演算子(<<)と比較(<)が同じ優先順序になるという面白いことが起きています。また、名前の最後の文字が":"のメソッドは右結合で、中置記法で書くと左右が逆になります。例えば

a :: b

b.::(a)

とみなされます(おそらく不変リストの定義のための仕様)。

宣言

変数

Scalaにはどこを参照するかを変更可能な変数と変更不可能な変数があり、それぞれvalとvarを使って定義します。例えば

val q : Int = 4 // q is of type Int and initialized with 4. The value of q cannot be changed.

var r : Int = 5 // r is of type Int and initialized with 5. One can modify the value of r by assignment (for example, "r = 3").

などと定義します。varで定義した方は例えば

r = 3

などとして値を変更することができます。
また、クラスのインスタンスを格納する変数をvalで定義した場合、どこを参照するかを変更することはできませんが、中身を変更することはできます。例えば

val arr = Array(1,2,3) // Initialized with an Int array with element {1,2,3}.
arr(0) = 4 // The first element becomes 4.

は正しくコンパイルできます。

クラス

Javaでは

public class AAA {
public int ff(int q) { /* ... */ }
}

だったのが、Scalaでは

class AAA {
def ff(q : Int) : Int { /* ... */ }
}

と書くことになります。(デフォルトでpublic)
staticメソッドは書けませんが、代わりにオブジェクトという、Javaでいうstaticメソッドしかないクラスを定義することができます。例えば、

object WW {
def gg(q : Int) : Int { /* ... */ }
}

で大体Java

public class WW {
public static int gg(int q) { /* ... */ }
}

と同じ意味です。


次は型システムと標準ライブラリについてです。

ラムダ式→SKIコンビネータ項

概要

ラムダ式をSKIコンビネータの式に変換するプログラムを書きました。
koba-e964/ski-comb · GitHub

やったこと

ラムダ式→SKIコンビネータの項の変換

実装は
高階ことりちゃんと学ぶSKIコンビネータ
を参考にしました。

Haskell風の書き方で説明します。やり方は上のリンク先に書いてあるので、ここでは実例だけ紹介します。
C = \x y z -> x (y z)
をSKIコンビネータ項に直してみましょう。
(1) 全てのλ抽象を新しく導入した関数に直す。このとき、新しく導入される関数の定義は、
関数名 自由変数... ラムダ式で束縛される変数
の形になる。
まずトップレベルの\x->...を直しましょう。

C = M
M x = \y z -> x (y z)

続いてM xの内部の\y -> ...を直します。

C = M
M x = N x
N x y = \z -> x (y z)

同様にして最終的には以下のようになります。

C = M
M x = N x
N x y = O x y
O x y z = x (y z)

(2) 関数の引数を消去してS,K,Iのみで表す
O x y z = x (y z)
O x y z = (K x z) (y z)
O x y z = S (K x) y z
O x y = S (K x) y
O x = S (K x)
O x = (K S x) (K x)
O x = S (K S) K x
O = S (K S) K

C=M=N=O*1より、結局
C = S (K S) K
がわかる。

課題


ここのやり取りで気付いたのですが、今のままだと実行時間も出力されるコードも線型よりも速いペースで増大します。現在のところどのくらいのペースで増大するのか見積もりができていないので、

  • 計算量・出力されるコードの大きさの増大の速さの見積もり
  • 高速化・サイズ削減

が目標になるかと思います。

*1:実際のコードではここもちゃんとやっているのでコードが肥大化します

ICPC 2014 Domestic

ICPC 2014 DomesticにAyatakaというチーム名で参加しました。
(メンバ:ばいなり(b_inary), うどん(kw_udon_), こば(kobae964))

A
うどんがやってくれました

B
私がやりました( Ideone.com - 2gTylp - Online C++ Compiler & Debugging Tool )

C
ばいなりがやってくれました

D
うどんと私がやりました ( Ideone.com - bJqf8d - Online C++ Compiler & Debugging Tool )

E
ばいなりがやってくれました

F
全員で考えました。
貪欲に残り回数が一番多い方向へ転がすという方針でやったら失敗しました。コンテスト終了後に7完したチームに解法を聞いたらあざやかでびっくり。

G
捨てました

こんな感じで5完13位( ACM-ICPC 2014 国内予選順位表 )でした。選ばれなかったAyataka(>_<)

モナド変換子の圏論的理解(Categorical understanding of monad transformers)

モナド変換子

Haskellにおいてモナド変換子(Monad transformer)は、以下の条件を満たすtです:

  • tのkindは(* -> *) -> * -> *
  • lift :: Monad m => m a -> t m aが定義されている
  • liftが以下の法則を満たす:
    1. lift . return = return
    2. m k. lift (m >>= k) = lift m >>= (lift . k)

(この定義を便宜上函数的定義(functional definition)と呼びます。)
この定義を圏論の言葉を使って書きなおすことを考えると、以下のようになります:

  • tのkindは(* -> *) -> * -> *
  • lift :: Monad m => m a -> t m aが定義されている
  • liftが以下の法則を満たす:
    1. liftはmからt mへの自然変換(natural transformation)になっている。つまり、
      • ∀(k :: a -> b). fmap k . lift = lift . fmap k
    2. liftはEndofunctorの圏におけるモノイド対象の準同型である。つまり、以下が成立する:
      • lift . return = return (単位元を保つ)
      • lift . join = join . fmap lift . lift (積を保つ)

(この定義を便宜上圏論的定義(categorical definition)と呼びます。)

この二つの定義が同値であることを示します。

函数的定義→圏論的定義

(1) lift . return = return
(2) ∀m k. lift (m >>= k) = lift m >>= (lift . k)
を仮定する。

(i) ∀(k :: a -> b). fmap k . lift = lift . fmap k

(2)においてk=return . fを代入すると
m f. lift (m >>= return . f) = lift m >>= (lift . return . f)
m f. lift (m >>= return . f) = lift m >>= (return . f) ((1)より)
fmap f m = m >>= return . fを利用すると
m f. lift (fmap f m) = fmap f (lift m)
f. lift . fmap f = fmap f . lift (mを消去)

(ii-i) lift . return = return

(1)から自明。

(ii-ii) lift . join = join . fmap lift . lift

(2)にk=idを代入すると
m. lift (m >>= id) = lift m >>= (lift . id)
m >>= id = join m, idは恒等射より
m. lift (join m) = lift m >>= lift
m >>= k = join (fmap k m)より
m. lift (join m) = join (fmap lift (lift m))
mを消去して
lift . join = join . fmap lift . lift

圏論的定義→函数的定義

読者の演習問題とする。(訳:疲れました)

追記(2014/06/25)要望があったので答えを載せます。(白い文字で書いているので選択すると読めます)
(i) ∀(k :: a -> b). fmap k . lift = lift . fmap k
(ii-i) lift . return = return
(ii-ii) lift . join = join . fmap lift . lift
を仮定する。

(1) lift . return = return

(i)から自明。

(2) ∀m k. lift (m >>= k) = lift m >>= (lift . k)

(以下白文字)

(i)の両辺に左からjoin . fmap liftを合成して
k. join . fmap lift . fmap k . lift = join . fmap lift . lift . fmap k
(ii-ii)を右辺に適用して
k. join . fmap lift . fmap k . lift = lift . join . fmap k
fmap (g . f) = fmap g . fmap fより
k. join . fmap (lift . k) . lift = lift . join . fmap k
両辺をmに適用して
m k. join (fmap (lift . k) (lift m)) = lift (join (fmap k m))
m >>= k = join (fmap k m)を利用して変形すると
m k. lift m >>= lift . k = lift (m >>= k)

Haskellでのエラー処理について(ErrorT, ExceptT)

Haskellインタプリタhttps://github.com/koba-e964/experiment/tree/master/typeinf )を書いていて、エラー処理をしたくなったのでモナド変換子ErrorTを導入しました。その後別の環境でコンパイルしてみたら

(前略) Use Control.Monad.Except instead (後略)

 と怒られてしまったのでびっくりして確認すると、どうやらmtlのバージョンがエラー処理を書いた環境は2.0以前、別の環境では2.2.0.1(2.2.1かも?記憶があいまい)だったのが原因だったようです。

このControl.Monad.Exceptというモジュールは、ここ2週間くらい前(2014/6/2)にリリースされたmtl-2.2.1 ( http://hackage.haskell.org/package/mtl-2.2.1 )で新たに導入されたようです。

 

新しく導入されたモナド変換子ExceptTと、以前からあったErrorT (Control.Monad.Error)との違いですが、見たところ型変数eに関する制約が無くなったというのが唯一の違いであるように思われます。ErrorTの各種インスタンス宣言には、

(Monad m, Error e) => MonadError e (ErrorT e m)

(Monad m, Error e) => Monad (ErrorT e m)

のように、Error eという宣言が必要でしたが、ExceptTのインスタンス宣言には必要ありません。(例:

Monad m => MonadError e (ExceptT e m)

Monad m => Monad (ExceptT e m)

など)