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)なんて返さないってことがわからない程度と言うべきか

Typed Racketのお勉強 (6)

4 Types in Typed Racket (続き)

いくつかの型を取る可能性がある変数や関数はUnion型になります

> (if (even? 37) 'yes 'no)
- : Symbol [more precisely: (U 'yes 'no)]
'no

'yesや'noを返す、っていうところまで見てるんですねえ
ってそういうの見ないと型推論とかできないか

こういう型がないとLisp伝統の、見つからなければ#fを返す、ってのが
できないですもんね

> member
- : (All (a)
      (->* (Any (Listof a)) ((-> a a Any)) (U False (Pairof a (Listof a)))))
#<procedure:member>

値の型はFalseか(Pairof a (Listof a))となってますね
(Pairof a (Listof a))っていうのは最低限ひとつの要素を持つリスト、って
意味でしょうか
そういえば関数を指定するところはAnyと指定されてますね
ほかには書きようはないんでしょうか

再帰的な型を定義することもできます

(define-type BinaryTree (U BinaryTreeLeaf BinaryTreeNode))
(define-type BinaryTreeLeaf Number)
(define-type BinaryTreeNode (Pair BinaryTree BinaryTree))

Typed Racketの型は階層化されていて、上位の型が期待されているところには
下位の型を入れることができます
上位の型をSupertype、下位の型をSubtypeと呼びます

• RealはIntegerのSupertype、IntegerはRealのSubtype、といった具合
• すべての型はAnyのSubtype
• もしある関数が別の関数と引数の数が同じで、引数がSupertypeで、値がSubtypeならその関数の型はもうひとつの関数のSubtype

小さな目標と細切れになった時間

ここんとこしばらく、小さな目標が達成するだけに近い状態なんですよね
10時半には眠くて目を開けていられなくなるんで

なぜだろう
午後カフェインを取らないようにしたから？
10時以降にスマホやノートPCを使わないようにしたから？

数学の本を読んでいるから、っていうのはなんかパターンにハマりすぎてる
気もするけどけっこうあるかもしれない

いずれにしろそれが本来の就寝時間ということなんだろうなあ
5時半起床なので7時間睡眠という計算

しかしちょっと時間が足りなさ過ぎる
すこし仕事が遅くなるだけでホントに達成するだけになったり
日曜はちょっと失敗でブログ書くのが遅くなってしまったし
細切れでちょっとずつやるのはホントは効率が良くないんだろうし

今はTyped Racketの話と、ガロアの数学の話と両方やろうとしているって
いうのがまた細切れを大きくしている

10時以降スマホやノートPCを使わない、にしてるので
10時でTyped Racketをやめて数学の本を読む、にしてて
それぞれ1日1回 IDE・エディタを開く、と1日1行 勉強ノートに何か書く、を
達成してるんだけど
まとめて達成できるように考えたほうがいいかなあ

Typed Racketの話をノートに書くとか
でもTyped Racketは本もないし
PCなしでどうやってTyped Racketの勉強をすればいいだろう
ドキュメントを印刷？

よく眠れた感さえあれば10時以降PC使ってもいいかなあ
実験してみるか
ちょっと前まではそうしてたんだし

失敗した

ビジネス手帳1小型版を買ったばっかりではありますが 

高橋 手帳 2018年 1月始まり ウィークリー ニューダイアリー ミニ 1 黒 No.133

ってのがあることにいまさら気が付きました

小型版サイズよりちょっとだけ縦長ですが
ポケットに入るサイズだし
ペンホルダーも着いてるし

こっちでよかったじゃないか・・・

ビジネス手帳1小型版を1年使うという選択肢もないではないですが
手帳を見るたびにアッチの方がよかったなと思いながら
1年を過ごすのはつらいのでやっぱり買いました

もったいないもったいない
何か使ってあげられる使いみちはないかな

Typed Racketのお勉強 (5)

4 Types in Typed Racket

主な基本型はInteger, Flonum, String, Char, Boolean, ->(関数)あたりですが
なんか妙に細かい型があります
数値型にPositiveとNegativeがある、くらいは理解できますが
こないだ出たZero型、One型の他にもTrue型とかある、というだけでなく
あらゆる値がすべてその値を型とできるようです

> 100
- : Integer [more precisely: Positive-Byte]
100
> (ann 100 100)
- : Integer [more precisely: 100]
100
> 0.1
- : Flonum [more precisely: Positive-Flonum]
0.1
> (ann 0.1 0.1)
- : Flonum [more precisely: 0.1]
0.1
> "aaa"
- : String
"aaa"
> (ann "aaa" "aaa")
- : "aaa"
"aaa"

これはどういう役に立つのかちょっとわかりません
型の理論とか勉強すると出てくるんでしょうか

Multiple Valueを返す場合の型は以下のようになります

> (lambda ([c : Char]) (values (string c) (char->integer c)))
- : (-> Char (values String Index))
#<procedure>

Index型というのは0からVectorのIndexの最大値までの整数を表す型らしいです

Rest Argumentのある関数の型はこの間やりました
型の後ろにアスタリスクをつけてました

Optional ArgumentやKeyword Argumentを含む関数の型は
->*を用いて書きます

デフォルト値を書いてやるとOptional引数になります

> (define (greet [given : String] [surname : String "Smith"])
    (string-append "Hello, " given " " surname))
> greet
- : (->* (String) (String) String)
#<procedure:greet>

ひとつめのカッコ内が普通のArgument、
ふたつめのカッコ内がOptional Argumentの型となります

最後にKeyword Argumentなんですが、例として

(->* (#:x Number) (#:y Number) (values Number Number))

という型が挙がっているんですけれども

> (define (kwarg #:x [x : Number] #:y [y : Number 3])
    (values x y))
> (kwarg #:x 2)
- : (values Number Number)
2
3
> (kwarg #:x 2 #:y 5)
- : (values Number Number)
2
5

という関数を作ってみたところ違う型の表示になりました

> kwarg
- : (-> #:x Number [#:y Number] (values Number Number))
#<procedure:kwarg>

例の通りの型定義をつけてやってもエラーにはならず
型の表示はさっきと変わらないので、書き方が違うだけで同じ型を表してるっぽいです

> (: kwarg (->* (#:x Number) (#:y Number) (values Number Number)))
> (define (kwarg #:x [x : Number] #:y [y : Number 3])
    (values x y))
> kwarg
- : (-> #:x Number [#:y Number] (values Number Number))
#<procedure:kwarg>

こどもの国（のアイスはおいしい＆ディアボロ）

今日は娘とこどもの国へ行ってきました

ここの楽しみはソフトクリーム
自分評価では史上最高
他では知らないなめらかさ
なんだろうこれは

こどもの国で売ってる牛乳は特別牛乳って言って
まあざっくりいうととても優れた牛乳ってことなんですが
実際おいしいし

でもそれでここまで違うか？

もうひとつ気づいたのは、特に夏場だとあっというまに
解け始めるということ
あまり温度が低くないのかな・・・？
これはなめらかさと関係するかもしれない

しかしあまりそういう評判を聞かないのが不思議
ヨメも同意してくれるんですが
娘はクリーム系拒否（昔は喜んで食べてたのになあ）

あと今日はジャグリング道具を貸し出してました
ディアボロ（中国ゴマ）・皿回し・お手玉の３種類

ディアボロはウチの娘でもとりあえず回すところまではできて
けっこう楽しんでいた模様

日頃本とマンガとゲームっていう子供なので
リアルの遊びに興味を持ったところを見ては見逃す訳にはいきません

さっそく安いやつを探してポチりました
これ

実際注文したのはヨドバシ・ドット・コムですが
送料ゼロだったので

こういうやつは安いだけで使いにくくては意味が無いんですが
それっぽい店が絶対の自信と言ってるので信用します
Amazonに700円くらいのもありましたがかなり心配
未経験だと、自分がヘタなのか道具がよくないのか判断できませんからね

楽しみ（自分もやる）