塾

娘がもうすぐ小4で入塾テスト受けたりするわけですが
これで実際に授業が始まると夜の8時まで塾とかになるんですよね
自分の小学生の頃を思い出すとこんなんでいいんだろうかという気がしなくもないです
現代の忙しすぎる子供たち、的な
そこまで詰め込んではいないですけど

とはいえそういうことも織り込み済みで決めたことなんで

塾で何を習うというよりもまずは普通に勉強する子供たちの間にいる、っていう
環境が大事かな、と思ってます
朱に交われば赤くなる、ってやつ
いい習慣が自然と身についてくれたらなあと

もちろん今時人気のある塾は考え方とか内容とかもいいと思いますし
先生の教え方もうまいですよね
きっといい感じになってくれるんじゃないかと

でもなんかこう、学校と塾両方ってちょっと大変かなとかもったいないなとか思います
塾に行ってたら学校のこの授業は免除、とかは無理かな
なんか上手くやったら先生も楽になったりしないですかね

TiddlyWiki 5も使ってます

パーソナルではWorkflowy依存ですがお仕事のメモには今TiddlyWiki 5を使ってます
クラウドにデータは置くなってことになってるんで

じゃあOneNote使えよって話ではありますが
どうも生理的に合わないところがありまして
グラフィカルで自由度が高くなるとどうもダメみたいです
ただ字を書くだけの方が楽
OneNoteだって字だけ書けばいいはずなんですけどね
どうもね

じゃあTiddlyWikiはどういうところがいいのかっていうと
上の反対ですべてテキストで書けるってのはあるんですが

何かとプログラマー（じゃないんですけどね）の心を揺さぶるような作り？

TiddlyWikiの記事はTiddlerっていうんですけど

あっちのTiddlerとこっちのTiddlerに同じことを書かなくていいように
Tranclusionっていうしくみを使って引用みたいなことができたりとか

JavaScriptで書かれた小さいコアがあって
あとは拡張スクリプトからタグから設定項目から
全部Tiddlerで書くようになってるとか

当然ながらその結果すごく拡張性が高くて
Wikiの文法までTiddlerで拡張できるとか
Wiki記法があんまり好きじゃなかったらMarkdownで書ける
プラグインなんかもあります（あんまり高機能なMarkdownじゃないけど

どうですか
そそりませんか

あとTiddlyWikiはIEさえあれば使えるってところがたまに強みです
つまりまっさらのWindows PCでも使えるってわけです
Officeすら入っていなくても
PCのセットアップなんかするときとか

IEとセットで使うなら.htaにしてしまうのが一番手っ取り早くて便利
TiddlyWikiはブラウザとの組み合わせによって保存が若干面倒になったりしますが
IE+.htaなら何も考えなくてすみます

っていうといつまでサポートされるのって話になりますけどね
うちの会社でIE禁止ってなるのはまあ当分先だと思われますので

Typed Racketのお勉強 (10)

5 Occurrence Typing

Occurrence Typingとはあまり聞き慣れない言葉
さらっとぐぐってみましたがそれっぽい言葉は見つかりませんでした
あまり普及してない概念なのかもしれません
Typed Closureってやつでも出てくるようです

無理に訳そうとせず進みます

なになに
述語の結果によって型をより正確に特定できるとな

(: flexible-length (-> (U String (Listof Any)) Integer))
(define (flexible-length str-or-lst)
  (if (string? str-or-lst)
      (string-length str-or-lst)
      (length str-or-lst)))

str-or-lstはStringか(Listof Any)かどちらかの
型であるというUnion型ですが
(string? str-or-lst)が#tを返したならば
str-or-lstはString型
そうでなければ消去法でstr-or-lstは(Listof Any)型だと
特定してくれるってことですね

だからこういうString型しか引数に取らない、または(Listof 何か)しか
引数にとれない関数にも渡せるよ、ってことでいいのかな

> string-length
- : (-> String Index)
#<procedure:string-length>
> length
- : (All (a) (-> (Listof a) Index))
#<procedure:length>

Occurrence Typingがない言語だとこういうのはどうなるんだっけ？
そもそも文字列型か何かのリストかどちらかを取る値っていうのも
めずらしい気がする、っていうか設計がおかしいかも、って思うかもだなあ

Typed Racketのお勉強 (9)

4 Types in Typed Racket (続き)

もうちょっと調べないともやっとするな・・・

前回よくわからなかったのがこれ
B ... BのふたつめのBがどうして必要なのかわからない

(: fold-left
   (All (C A B ...)
        (-> (-> C A B ... B C) C (Listof A) (Listof B) ... B
            C)))

1.6 Other Type Constructors  にそれっぽいのを発見

Rest argumentsに異なる型が含まれるケースはこれにあたる

(-> dom ... rest ooo bound rng)

rest oooの部分がRest Arguments
oooっていうのは単に...という文字のこと
つまりrest ooo boundがB ... Bに対応してるってことになる
定義上はふたつめのB（か、すくなくともそこに何か）が必要っぽい

説明

... the third form specifies a non-uniform rest argument of type rest with bound bound. The bound refers to the type variable that is in scope within the rest argument type.

何を言っているのかよくわからない
わからないけどわからないまま日本語に直してみる

3番目のフォーム（上に引用したやつ）は rest型の一様でないrest argumentをboundにバインドするよう指定する。このバインドはrest argumentの型のスコープ内にある型変数を参照する。

うんやっぱりわからない
ふたつめのBがなくてもB ...だけでもわかるんじゃないの？

わからないのでふたつめのBをDに変えてみたりとか

(: fold-left
   (All (C A B ...)
        (-> (-> C A B ... D C) C (Listof A) (Listof B) ... D
            C)))

これはエラー

Type Checker: parse error in type;
 used a type variable not bound with ... as a bound on a ...
  variable: D in: (-> (-> C A B ... D C) C (Listof A) (Listof B) ... D C)

「...にバインドされてない変数を...へのバインドとして使った」てことですかね
Bは...にバインドされるんだということはわかった

ふたつめのBを消してやっても動くし
上の定義にしたがえば、これはCがboundに対応して
関数の値の型がなくなってしまうはずなんだけどどうなってるの

(: fold-left
   (All (C A B ...)
        (-> (-> C A B ... C) C (Listof A) (Listof B) ...
            C)))

型を見てみる

> fold-left
- : (All (C A B ...) (-> (-> C A B ... B C) C (Listof A) (Listof B) ... B C))
#<procedure:fold-left>

ふたつめのBが補完されてるし
型推論のおかげかな

B以外に書けないし書かなくてもBが補完されるなら
どうしてBを書かなきゃいけないの
そしてBにバインドしてそれをどうするの

(All (a ... a ooo) t)

こっちは単に型tをパラメータ化したもの、というだけしか書いてない

うーん

NHK GJ

今日はNHKで精霊の守り人の特集みたいなのやってましたね

上橋菜穂子の本を読んだのはごく最近、しかも守り人シリーズじゃなくて
獣の奏者の方だったりするんですけど
このひとの書いたものなら間違いないっていう感覚です（何様

精霊の守り人シリーズはとりあえず精霊の守り人だけ軽装版を買ってあったんで
あやせはるか、びじんーーーっていう反応を見てすかさず
ほらウチにもあるよ、と言って渡してあげたらけっこう食いついてました

本当の狙いは上橋菜穂子じゃなくて
モモとかはてしない物語を読んでもらうことなんですけど
まずはお姫さまが主人公じゃないファンタジーに慣れさせることかなあ、と思って

獣の奏者は全巻あるんですがちょっとまだ早いかなあ
読むならもうなんだっていいと思ってたりするんですが
きっかけがあれば何でも読みそうなんで

Typed Racketのお勉強 (8)

4 Types in Typed Racket (続き)

Rest argumentsの単純なケース
（この前もちょっと出てきてましたが）
*で0個以上の繰り返しであることを示してます

(: sum (-> Number * Number))
(define (sum . xs)
  (if (null? xs)
      0
      (+ (car xs) (apply sum (cdr xs)))))

引数の型が異なってくる場合

(: fold-left
   (All (C A B ...)
        (-> (-> C A B ... B C) C (Listof A) (Listof B) ... B 
            C)))
(define (fold-left f i as . bss)
  (if (or (null? as)
          (ormap null? bss))
      i
      (apply fold-left
             f
             (apply f i (car as) (map car bss))
             (cdr as)
             (map cdr bss))))

わからないことがふたつ

Bは出てくる場所によって違う型を指してる？それともAnyみたいなもの？
B ... Bの最後のBは必要？

> (fold-left + 0 '(1 2 3 4) '(5 6 7 8))
- : Integer [more precisely: Nonnegative-Integer]
36
> (fold-left (λ (i v n s) (string-append i (vector-ref v n) s))
             ""
             (list (vector "A cat" "A dog" "A mouse")
                   (vector "tuna" "steak" "cheese"))
             (list 0 2)
             (list " does not eat " "."))
Type Checker: type mismatch
  expected: String
  given: Any in: i
Type Checker: Polymorphic function `vector-ref' could not be applied to arguments:
Types: VectorTop Integer -> Any
Arguments: Any Any
Expected result: String
 in: (vector-ref v n)
Type Checker: type mismatch
  expected: String
  given: Any in: s
Type Checker: Summary: 3 errors encountered in:
  i
  (vector-ref v n)
  s

ダメじゃないですか
例のとおりに入れたのに・・・

λに型を入れてやったら動いたんですけど

> (fold-left (λ ([i : String]
                 [v : (Vector String String String)]
                 [n : Integer]
                 [s : String]) : String
               (string-append i (vector-ref v n) s))
             ""
             (list (vector "A cat" "A dog" "A mouse")
                   (vector "tuna" "steak" "cheese"))
             (list 0 2)
             (list " does not eat " "."))
- : String
"A cat does not eat cheese."

でもめんどくさいよ？
例の通りで動かないのはどうして？

確かにこう書いてはあったけど・・・
めんどくさいよ？

こんなときには型修飾が必要と書いてあります

• 関数をdefineするとき
• lambdaを直接変数にバインドするとき
• lambdaを多相関数の引数にするとき
• ミュータブルな変数を定義するとき

単純な例では動いたんだし

Bは出てくる場所によって違う型を指してる？それともAnyみたいなもの？

エラーメッセージからするとAnyではないっぽい気がする

B ... Bの最後のBは必要？

取っても動いた
なんでついてるの？

もうちょっと調べないともやっとするな・・・

Typed Racketのお勉強 (7)

4 Types in Typed Racket (続き)

Typed Racketはパラメータ多相にも対応しています

Maybeモナドっぽいもの

(struct None ())
(struct (a) Some ([v : a]))
(define-type (Opt a) (U None (Some a)))

(struct (a) ...)は型aを引数に取った型の定義

型だけ作ってもモナドにはならないとは思いますが
使い方の例にはなりますね

(: find (-> Number (Listof Number) (Opt Number)))
(define (find v l)
  (cond [(null? l) (None)]
        [(= v (car l)) (Some v)]
        [else (find v (cdr l))]))

このfind、これで終わりじゃないよな？
当然、数以外にも適用できるようにするはず・・・

流れ的に次は多相関数
でも例はfindじゃないな・・・

(: list-length (All (a) (-> (Listof a) Integer)))
(define (list-length l)
  (if (null? l)
      0
      (add1 (list-length (cdr l)))))

lの要素がなんだろうが気にしないので

どれ

> (list-length '(1 2 3 4))
- : Integer
4
> (list-length '("a" "b" "c" "d"))
- : Integer
4

こういうのはどうなるんだろう？

> (list-length '(1 2 "c" "d"))
- : Integer
4

許されるんだな

findは放置みたいなので自分で書き直してみよう

=は数にしか使えないので・・・

> =
- : (-> Number Number Number * Boolean) ... [Use (:print-type <expr>) to see more.]
#<procedure:=>

:print-typeしてみろって言ってる

> (:print-type =)
(case->
 (-> Real Real-Zero Boolean)
 (-> Real-Zero Real Boolean)
 (-> Exact-Number One Boolean)
 (-> One Exact-Number Boolean)
 (-> Exact-Number Positive-Byte Boolean)
 (-> Positive-Byte Exact-Number Boolean)
 (-> Exact-Number Byte Boolean)
 (-> Byte Exact-Number Boolean)
 (-> Exact-Number Positive-Index Boolean)
 (-> Positive-Index Exact-Number Boolean)
 (-> Exact-Number Index Boolean)
 (-> Index Exact-Number Boolean)
 (-> Exact-Number Positive-Fixnum Boolean)
 (-> Positive-Fixnum Exact-Number Boolean)
 (-> Exact-Number Nonnegative-Fixnum Boolean)
 (-> Nonnegative-Fixnum Exact-Number Boolean)
 (-> Exact-Number Negative-Fixnum Boolean)
 (-> Negative-Fixnum Exact-Number Boolean)
 (-> Exact-Number Nonpositive-Fixnum Boolean)
 (-> Nonpositive-Fixnum Exact-Number Boolean)
 (-> Exact-Number Fixnum Boolean)
 (-> Fixnum Exact-Number Boolean)
 (-> Exact-Number Positive-Integer Boolean)
 (-> Positive-Integer Exact-Number Boolean)
 (-> Exact-Number Nonnegative-Integer Boolean)
 (-> Nonnegative-Integer Exact-Number Boolean)
 (-> Exact-Number Negative-Integer Boolean)
 (-> Negative-Integer Exact-Number Boolean)
 (-> Exact-Number Nonpositive-Integer Boolean)
 (-> Nonpositive-Integer Exact-Number Boolean)
 (-> Exact-Number Integer Boolean)
 (-> Integer Exact-Number Boolean)
 (-> Exact-Number Positive-Exact-Rational Boolean)
 (-> Positive-Exact-Rational Exact-Number Boolean)
 (-> Exact-Number Nonnegative-Exact-Rational Boolean)
 (-> Nonnegative-Exact-Rational Exact-Number Boolean)
 (-> Exact-Number Negative-Exact-Rational Boolean)
 (-> Negative-Exact-Rational Exact-Number Boolean)
 (-> Exact-Number Nonpositive-Exact-Rational Boolean)
 (-> Nonpositive-Exact-Rational Exact-Number Boolean)
 (-> Exact-Number Exact-Rational Boolean)
 (-> Exact-Rational Exact-Number Boolean)
 (-> Exact-Number Exact-Number Boolean)
 (-> Exact-Number Exact-Number Boolean)
 (-> Real Real-Zero Boolean)
 (-> Real-Zero Real Boolean)
 (-> Real Positive-Real Boolean)
 (-> Positive-Real Real Boolean)
 (-> Real Nonnegative-Real Boolean)
 (-> Nonnegative-Real Real Boolean)
 (-> Real Negative-Real Boolean)
 (-> Negative-Real Real Boolean)
 (-> Real Nonpositive-Real Boolean)
 (-> Nonpositive-Real Real Boolean)
 (-> Real Real Boolean)
 (-> Real Real Boolean)
 (-> Number Number Number * Boolean))

どわ！

いろんな型の比較ができる、っていいたいの？
(-> Number Number Number * Boolean)だけで全部カバーできてるような
気もするけど？
複数を比較できるのが(-> Number Number Number * Boolean)だけだから
他は`(-> Number Number Number * Boolean)から呼び出されて使われる、
って感じなのかな？

まあそれはおいといてequal?で比較することに

> equal?
- : (-> Any Any Boolean)
#<procedure:equal?>
> (:print-type equal?)
(-> Any Any Boolean)

こっちは普通
こうね

(: find2 (All (a) (-> a (Listof a) (Opt a))))
(define (find2 v l)
  (cond [(null? l) (None)]
        [(equal? v (car l)) (Some v)]
        [else (find2 v (cdr l))]))

お試し

> (find2 3 '(1 2 3 4))
- : (U None (Some Positive-Byte))
#<Some>
> (find2 5 '(1 2 3 4))
- : (U None (Some Positive-Byte))
#<None>
> (find2 'c '(a b c d))
- : (U None (Some (U 'c 'a 'b 'd)))
#<Some>
> (find2 'e '(a b c d))
- : (U None (Some (U 'c 'a 'b 'd 'e)))
#<None>
> (find2 '(c d) '((a b) (b c) (c d) (d e)))
- : (U None (Some (U (List 'c 'd) (List 'a 'b) (List 'b 'c) (List 'd 'e))))
#<Some>
> (find2 '(e f) '((a b) (b c) (c d) (d e)))
- : (U None
       (Some
        (U (List 'c 'd) (List 'a 'b) (List 'b 'c) (List 'd 'e) (List 'e 'f))))
#<None>

おｋ

最後、(U (List 'c 'd) (List 'a 'b) (List 'b 'c) (List 'd 'e) (List 'e 'f)))を
返すかも、っていうのはどこまでプログラムの中身がわかってるのかなあ
(List 'e 'f)を見つけてくるなんてすごいと言うべきか
(List 'e 'f)なんて返さないってことがわからない程度と言うべきか