|> in Scala

F# の |> を Scala でやってみた。

scala> class Holder[A](a:A) {
     |   def |>[B](f:A => B) = f(a)
     | }
defined class Holder

scala> implicit def any2holder[A](a:A) = new Holder(a)
any2holder: [A](a: A)Holder[A]

scala> val succ = (x:Int) => x + 1
succ: (Int) => Int = <function1>

scala> 3 |> succ |> succ
res0: Int = 5

scala> 3 |> { (x:Int) => x * 2 } |> succ
res1: Int = 7

お、これは・・・

scala> 3 |> {
     |   case x => x * 2
     | }
res2: Int = 6

scala> 3 match {
     |   case x => x * 2
     | }
res3: Int = 6

おお！match と同じように使える！

• 追記

scala> class Holder[A](a:A) {
     |   def |>[B](f:A=>B) = f(a)
     |   def <|:[B](f:A=>B) = f(a)
     | }
defined class Holder

scala> implicit def any2holder[A](a:A) = new Holder(a)
any2holder: [A](a: A)Holder[A]

scala> val succ = (x:Int) => x + 1
succ: (Int) => Int = <function1>

scala> succ <|: succ <|: 10
res0: Int = 12


scala> val tw = (x:Int) => x * 2
tw: (Int) => Int = <function1>

scala> succ <|: succ <|: 10 |> tw |> tw
res1: Int = 48

scala> tw <|: tw <|: 10 |> succ |> succ
res2: Int = 42

おー！

矛盾

楚人に盾と矛とを鬻（ひさ）ぐ者有り。之（これ）を誉めて（ほめて）曰く「吾が盾の堅きこと、能く（よく）陥す（とほす）もの莫し（なし）」と。また、その矛をほめていはく、「わが矛の利なること、物において陥（とほ）さざることなきなり。」と。あるひといはく、「子の矛を以て、子の盾を陥（とほ）さばいかん。」と。その人応ふること能はざりき。

矛盾 - Wikipedia

Theorem 矛盾 : forall (矛 盾:Type)(突き通す:矛 -> 盾 -> Prop),
 (exists 最強の矛:矛, forall あらゆる盾:盾, 突き通す 最強の矛 あらゆる盾) ->
 (exists 最強の盾:盾, forall あらゆる矛:矛, ~ 突き通す あらゆる矛 最強の盾) ->
 False.
Proof.
 intros 矛 盾 突き通す.
 intros どんな盾でも貫く矛がある どんな矛でも防ぐ盾がある.
 elim どんな盾でも貫く矛がある.
 intros 最強の矛 最強の矛はあらゆる盾を貫く.
 elim どんな矛でも防ぐ盾がある.
 intros 最強の盾 最強の盾はあらゆる矛を防ぐ.
 apply (最強の盾はあらゆる矛を防ぐ 最強の矛).
 apply (最強の矛はあらゆる盾を貫く 最強の盾).
Qed.

NotNull

NotNull型を継承すれば、自分で作った型に関しては、nullが入らないことを静的に保証することができます。 class X extends NotNull { ... } とすると、X型の変数にはnullが入れられません。

http://twitter.com/kmizu/status/21992714816

やってみる。

scala> val f:String = "a"
f: String = a

scala> val f:String = null
f: String = null

scala> val f:String with NotNull = "a"
f: String with NotNull = a

scala> val f:String with NotNull = null
<console>:4: error: type mismatch;
 found   : Null(null)
 required: String with NotNull
       val f:String with NotNull = null

おー！

scala> def hoge(s:String) = "hoge" + s
hoge: (String)java.lang.String

scala> hoge("aa")
res2: java.lang.String = hogeaa

scala> hoge("")
res3: java.lang.String = hoge

scala> hoge(null)
res4: java.lang.String = hogenull

scala> def hoge2(s:String with NotNull) = "hoge" + s
hoge2: (String with NotNull)java.lang.String

scala> hoge2("aa")
res5: java.lang.String = hogeaa

scala> hoge2("")
res6: java.lang.String = hoge

scala> hoge2(null)
<console>:6: error: type mismatch;
 found   : Null(null)
 required: String with NotNull
       hoge2(null)

おーー！
これはいい！

• 追記

NotNull から Nullable への変換はやってくれるが、
Nullable から NotNull への変換はやってくれない。
(そりゃそっか)

scala> class A
defined class A

scala> val a:A with NotNull = new A
<console>:5: error: type mismatch;
 found   : A
 required: A with NotNull
       val a:A with NotNull = new A
                              ^
scala> val a = new A with NotNull
a: A with NotNull = $anon$1@5561bfa3

Coqりさん 証明のかけら

Coq りさん Coq りさん、フィボナッチ数列の末尾再帰にしたやつって、本当に元のと同じなんですか？

Fixpoint fib1 (n : nat) : nat :=
 match n with
  | 0 => 0
  | 1 => 1
  | S n => fib1 n + fib1 (pred n)
 end.

Fixpoint fib2 (a b n : nat) : nat :=
 match n with
  | 0 => a
  | S n => fib2 b (a + b) n
 end.

Theorem fib_eq : forall (n:nat), fib1 n = fib2 0 1 n.
Proof.
  intro n.
  induction n.
    simpl.
    reflexivity.
    
    (*´・ω・｀*)
Qed.

れんしう

∃a∀b[P(a, b)] → ∀b∃a[P(a, b)]

Lemma exists_forall : forall (A:Type)(P: A -> A -> Prop),
  (exists a:A, forall b:A, P a b) -> (forall b:A, exists a:A, P a b).
Proof.
  intros A P H1 a.
  elim H1.
  intros x H2.
  exists x.
  apply H2.
Qed.

Maybe/Option のリストから普通のリストへ

Ocaml の時は自作したけど、Scala と Haskell は結構簡単にできる。

↓Scala

scala> List(Some(4), Some(2), None, Some(9), None, Some(0)) flatMap (x => x)
res0: List[Int] = List(4, 2, 9, 0)

↓Haskell

> [Just 4, Just 2, Nothing, Just 9, Nothing, Just 0] >>= maybe [] return
[4,2,9,0]

ただ、Haskell は普通に bind id しようとすると怒られる。

> [Just 4, Just 2, Nothing, Just 9, Nothing, Just 0] >>= id

<interactive>:1:55:
    Couldn't match expected type `[b]' against inferred type `Maybe t'
    In the second argument of `(>>=)', namely `id'
    In the expression: [Just 4, Just 2, Nothing, Just 9, ....] >>= id
    In the definition of `it':
        it = [Just 4, Just 2, Nothing, ....] >>= id

for/do 構文を使っても書ける。
実際、TDDBC 名古屋初日の、自分の卓の Scala 組は for 式を上手いこと使っていた。

OCaml ももっと自由に使えるように勉強していこう。

遊んだ

久々に (?) Scala で遊んでみる。

• 再帰さん

scala> def z[A,B](f: (A=>B) => (A=>B)): A=>B = (x:A) => f(z(f))(x)
z: [A,B](((A) => B) => (A) => B)(A) => B

scala> z { (f:Int=>Int) => (n:Int) => if (n < 2) n else n * f(n - 1) } (10)
res2: Int = 3628800

scala> z { (f:List[Int]=>List[Int]) => (xs:List[Int]) => xs match {
     |   case Nil => Nil
     |   case x :: xs =>
     |     val (l,r) = xs partition (_ <= x)
     |     f(l) ::: (x :: f(r))
     | }} { List(3,4,6,7,6,543,466,433,75,231,544,212,3,4,3) }
res3: List[Int] = List(3, 3, 3, 4, 4, 6, 6, 7, 75, 212, 231, 433, 466, 543, 544)

qsort はよく filter 使うけど、partition なんてのもあるのか。

• 論理値を関数っぽく

scala> implicit def boolToProc(b: Boolean) = {
     |   def if_(t: => Unit)(f: => Unit) = if (b) t else f
     |   if_ _
     | }
boolToProc: (Boolean)(=> Unit) => (=> Unit) => Unit

scala> (2 < 3) { println("hoge") } { println("piyo") }
hoge

scala> (4 < 3) { println("hoge") } { println("piyo") }
piyo

本当は、値返せるようにしたかったけど、

scala> implicit def boolToFunc[A](b: Boolean): (=> A) => (=> A) => A = {
     |   def k[A1,A2](x: => A1)(y: => A2) = x
     |   def f[A1,A2](x: => A1)(y: => A2) = y
     |   if (b) k _ else f _
     | }
boolToFunc: [A](b: Boolean)(=> A) => (=> A) => A

scala> (2 < 3) { 23 } { 34 }
<console>:7: error: type mismatch;
 found   : Int(23)
 required: A
       (2 < 3) { 23 } { 34 }

んー・・・・・・

• 追記

id:jmtaro さんがScala で論理値を関数っぽく、の勝手に続きでやってくれました。
なるほど、apply という手がありましたか。その辺の存在をすっかり忘れていた・・・

scala> implicit def boolToFunc(b: Boolean) = new {
     |   def apply[A](x: => A)(y: => A) = if (b) x else y
     | }
boolToFunc: (Boolean)java.lang.Object{def apply[A](=> A)(=> A): A}

scala> (2 < 3){ 23 }{ 34 }
res0: Int = 23

scala> (4 < 3){ 23 }{ 34 }
res1: Int = 34

ほほーう。

liftとか

liftで遊んでみる。

> :t map
map :: (a -> b) -> [a] -> [b]
> :t fmap
fmap :: (Functor f) => (a -> b) -> f a -> f b
> :t liftM
liftM :: (Monad m) => (a1 -> r) -> m a1 -> m r
> :t liftM2
liftM2 :: (Monad m) => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
> :t ap
ap :: (Monad m) => m (a -> b) -> m a -> m b

> :t liftM (+)
liftM (+) :: (Num a1, Monad m) => m a1 -> m (a1 -> a1)
> :t liftM2 (+)
liftM2 (+) :: (Num a1, Monad m) => m a1 -> m a1 -> m a1
> :t liftM2 id
liftM2 id :: (Monad m) => m (a2 -> r) -> m a2 -> m r

> liftM2 (+) [1..4] [3,4]
[4,5,5,6,6,7,7,8]
> liftM (+) [1..4] `ap` [3,4]
[4,5,5,6,6,7,7,8]
> ap [succ,(*2)] [1..4]
[2,3,4,5,2,4,6,8]

> :t liftM (+) [1..4]
liftM (+) [1..4] :: (Num a1, Enum a1) => [a1 -> a1]

> map (\f -> f 10) (liftM (+) [1..4])
[11,12,13,14]
> liftM (+) [1..4] >>= return . (\f -> f 10)
[11,12,13,14]

Proof Cafe

4/25に、Proof Cafe (栄)に参加してきました。

Coq 初体験。
最初は、id:yoshihiro503 さんから資料に沿って Coq の解説が。

Vernacular が分かれば Coq が分かる？
Coq のファイルの拡張子は .v
Checkで 型を調べる。
ガリナ(Gallina)：ラムダ式
nat : 型を表すラムダ式 (自然数) - Gallina 、この型はSet。
Set : 型を表すラムダ式 (型)、この型はType。
Type : 型を表すラムダ式 (型)、この型はType。
Prop : 命題の型

Eval compute in 〜 で、〜を評価できる。

その後、これをやってみる。
↓書いたやつ。

(* listの定義 *)
Inductive list (A: Type) : Type :=
 | nil  : list A
 | cons : A -> list A -> list A.
(* Check (cons nat 3 (nil nat)). *)

(* 型推論させる *)
Implicit Arguments nil [A].
Implicit Arguments cons [A].
(* Check (cons 3 nil). *)

(* append(再帰関数)の定義 *)
(* 型を中括弧で指定すると、型推論が効く。 *)
(* 型を小括弧で指定すると型推論が効かないけど、あとでImplicitすればできる *)
Fixpoint append {A : Type} (xs ys: list A) : list A :=
 match xs with
 | nil => ys
 | cons x xs => cons x (append xs ys)
 end.
(* 中置演算子++の定義。append関数に別名を与える。 *)
(* at level は結合の強さ*)
Infix "++" := append (at level 60).

Fixpoint length {A : Type} (xs : list A) : nat :=
 match xs with
 | nil => O
 | cons x xs => S (length xs)
 end.

Theorem append_assoc : forall (A: Type) (xs ys zs : list A),
 (xs ++ ys) ++ zs = xs ++ (ys ++ zs).
Proof.
 intros.
 induction xs.
  simpl.
  reflexivity.
  simpl.
  
  rewrite IHxs.
  reflexivity.
Qed.

Theorem append_length : forall (A: Type) (xs ys: list A),
  length (xs ++ ys) = length xs + length ys.
Proof.
 intros.
 induction xs.
  simpl.
  reflexivity.
  
  simpl.
  rewrite IHxs.
  reflexivity.
Qed.

simpl 賢い。すごく賢い。

IHxs が lHxs に見えて、lHxsって書いてたら通らなくて、しばらく（・３・）アルェー ってなってた。
IH は「Induction Hypothesis (帰納法の仮定)」の略。

関数合成・・・

. こわい。

> ((.) . (.)) succ (+) 1 2
4
> ((.) . (.)) length (++) "hoge" "piyo"
8
> ((.) (.)) (+) 1 succ 2
4