手帳＆工作

ここ何年かビジネス手帳1ばかり、と書いておきつつ来年は小型版を使ってみることに 

高橋 手帳 2018年 1月始まり ウィークリー ビジネス手帳 小型版 1 黒 No.140

ひとえにサイズの問題
バッグが変わって、アクセスのいいポケットの口のサイズが
若干ギリギリになったため

小型版なら余裕
最近の記入量なら小型版でもいけそうだなと

さてこいつはペンホルダーがついてないのが弱点
小さいからっていうのはあるかもしれないけど・・・

そこでここに差してみることを考えました

しかしこれはでっぱり具合が若干問題外

そこで思い切ってこんな風にしてみました

これならまあなんとか？

美しいとはちょっと言えませんが
耐久力もちょっと心配ですが
とりあえずこれで行ってみようかと

ダメだったらカバーをつける作戦もあるし

Typed Racketのお勉強 (4)

3 Specifying Types の続き

(let ([x : Number 3]) (add1 x))

は、こういう風に書くこともできます

(let ([#{x : Number} 3]) (add1 x))

こちらの書き方を使うと、前者の書き方に対応してない式でも
型を示すことができます

(: assert-symbols! ((Listof Any) -> (Listof Symbol)))
(define (assert-symbols! lst)
  (match lst
    [(list (? symbol? #{s : (Listof Symbol)}) ...) s]
    [_ (error "expected only symbols, given" lst)]))

matchがわかりません
パターンマッチしてるんだろうということまでは予想できますが
(list (? symbol? #{s : (Listof Symbol)})って？

The Racket Guideの12 Pattern Matchingを見てみます
(list ...)はリストにマッチすることはわかりましたがそこまで
The Racket Referenceの9 Pattern Matchingによると
（list (? symbol?) ...）はリストの各要素がsymbol?であるときにマッチ
（list (? symbol? #{s : (Listof Symbol)}) ...）は
リストの各要素がsymbol?であって
さらに#{s : (Listof Symbol)}であるときにマッチ

#{s : (Listof Symbol)}というのがここで出てきた書き方ですね
型を指定しないならば(list (? symbol? s) ...)で
sに値がバインドされるようですが、matchは
(list (? symbol? s : (Listof symbol)) ...)という書き方に
対応していないので#{}を使った書き方を使う・・・と

symbol?はリストの要素ひとつひとつに適用されていると思うんですが
sはリスト全体にバインドされているというのがちょっと不思議で
飲み込めてませんけど
そのへんは実際matchを使いたくなったときにもう一回見ます

それにしてもmatchが対応していないから#{}を使えば型を
マッチできる、っていったい中身はどうなっているのか
ちょっと想像がつきません
Macro Stepperでリーダーマクロが展開されたところが見えたりするだろうか、と
思いましたが型が取れただけでした → [(list (? symbol? s) ...) s]

まあこのへんにして先に進みます

式の型を指定してやることもできます
変な型にはできません

> (+ 7 1)
- : Integer [more precisely: Positive-Index]
8
> (ann (+ 7 1) Number)
- : Number
8
> (ann (+ 7 1) String)
Type Checker: type mismatch
  expected: String
  given: Positive-Index in: (+ 7 1)

型推論の話も出てきました
こんなときには型修飾が必要と書いてあります

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

このあいだidは宣言無しで定義できたのになあ、と思ったんですが

> (define (f x) (+ x 1))
Type Checker: type mismatch
  expected: Number
  given: Any in: x

(f x)のxはAny型、(+ x 1)のxはNumber型と思っているようです
idのときはどっちもAny型だったからたまたまエラーにならなかった、って
ことですかね

Typed RacketっていうのはRacketの拡張なはずなんですが
どこまで拡張できるようになってるんでしょうか
すごいにも程がある

オブジェクトシステムがマクロで書けるなら
型だって型推論だってマクロで書けるでしょ、って感覚なんでしょうか
Racketはリーダーを完全に置き換えられる、というのを聞いたことが
あります
その辺も関係してるんでしょうか
わかりません

最後に型名の定義
define-typeを使います

(define-type NN (-> Number Number))

どれどれ

> (: add2 NN)
> (define (add2 n) (add1 (add1 n)))
> (add2 3)
- : Number
5

define-typeで定義した型と元の型は同じなんでしょうか
元の型に展開される、と書いてありますので同じなんでしょうね

一応軽く試してみます

> (define-type N Number)
> (: add3 (-> N N))
> (define (add3 n) (+ n 3))
> (define five : Number 5)
> five
- : Number
5
> (add3 five)
- : Number
8

やっぱりまったく同じものとして扱われてるみたいですね

> add3
- : NN
#<procedure:add3>

add3は(-> N N)型として定義したのにNN型ということにされてしまいました

喜ぶべきか

今日娘からLINEがありましてね

限定BOX勧誘で選択UR取ったって言うんですよ
しばらくかかって貯めた石50個使って
一発で

この強運娘が

帰ったらそれはもう嬉しそうな顔でお出迎え
寝るまでテンション上がりっぱなし

ちょっと複雑なところでもあるんですけどね
将来ガチャにハマったりしないだろうか、みたいな
フルコンボしたとかで喜んでくれたほうがこっちも素直に喜べるんだけどなー

Typed Racketのお勉強 (3)

3 Specifying Types の続き

前回、型を指定しないで定義したidの型を見るのを忘れてました

> (define (id z) z)
> id
- : (-> Any Any)
#<procedure:id>

Any型というのがあるんですね

次はlambdaの修飾

> (lambda ([x : Number]) : Number (+ x 5))
- : (-> Number Number)
#<procedure>
> ((lambda ([x : Number]) : Number (+ x 5)) 3)
- : Number
8

.を使った引数の指定は型名の後に*をつけます

> (lambda ([x : Number] . [y : Number *]) : Number (apply + x y))
- : (-> Number Number * Number)
#<procedure>
> ((lambda ([x : Number] . [y : Number *]) : Number (apply + x y)) 1 2 3)
- : Number
6

case-lambdaも同様
と言われてもcase-lambdaて何
引数の数で場合分けしてくれるlambdaのようです

> (case-lambda [() 0]
               [([x : Number]) x])
- : (case-> (-> Number Number) (-> Zero))
#<procedure>

case-lambdaはcase->型で、それぞれのcaseを関数型としてとるんですね
そして0はNumber型ではなくZero型なのか

練習も兼ねて

> ((case-lambda [() 0]
              [([x : Number]) x]))
- : Integer [more precisely: Zero]
0

Zero型ね

> ((case-lambda [() 0]
                [([x : Number]) x]) 1)
- : Integer [more precisely: One]
1

え、One型もあるの

> 0
- : Integer [more precisely: Zero]
0
> 1
- : Integer [more precisely: One]
1
> 2
- : Integer [more precisely: Positive-Byte]
2

さすがにTwo型はなかった
0と1だけ特別扱いなんだな

引数の数が合わない場合もやっとこう

> ((case-lambda [() 0]
              [([x : Number]) x]) 1 2)
Type Checker: No function domains matched in function application:
Domains: 
         Number
Arguments: One Positive-Byte
 in: ((case-lambda (() 0) (((x : Number)) x)) 1 2)

そりゃそうだ

Typed Racketのお勉強 (2)

3 Specifying Types

:を使った修飾は値の定義やローカルの定義でも使えます

(let ()
  (: x Number)
  (define x 7)
  (add1 x))

たいていのバインド式は式の中でも型を書けるようになっています

(define x : Number 7)
(define (id [z : Number]) : Number z)

どっちが推奨とかあるんですかね
言ってもらえないと気になって夜も眠れません（眠れます
どっちかというと前者の書き方のほうが見やすい気がします

この例を見てidに型はつけたくないなあとか思ったり
よけいな話でした

letやその変種(letrecとか)でのバインドにも型修飾が付けられます

> (let ([x : Number 3]) (add1 x))
- : Number
4

つけられます、というからにはつけなくてもいいんだっけ？

> (let ([x 3]) (add1 x))
- : Integer [more precisely: Positive-Index]
4

動きますね
型は推論してくれているっぽい

トップレベルの定義も別に型いらないんだったかな？

> (define y 5)
> y
- : Integer [more precisely: Positive-Byte]
5
> (define (id z) z)
> (id 3)
- : Integer [more precisely: Positive-Byte]
3
> (id "aaa")
- : String
"aaa"

ふーんそうだったか

Typed Racketのお勉強 (1)

Typed RacketはRacketに型を付けたものです

The Typed Racket Guideを見ながら勉強していきます
詳細はThe Typed Racket Referenceに

1 Quick Start

とりあえずこれをやれと

• ソース先頭の#lang racketを#lang typed/racketに変える
• (require mod)を(require typed/mod)に変える
• Structureの定義およびトップレベルの定義を型で修飾する

例

#lang typed/racket

(struct pt ([x : Real] [y : Real]))

(: distance (-> pt pt Real))
(define (distance p1 p2)
  (sqrt (+ (sqr (- (pt-x p2) (pt-x p1)))
           (sqr (- (pt-y p2) (pt-y p1))))))

->が関数ってことですね
どことなくHaskellっぽい

どれどれ

> (distance (pt 0 0) (pt 3 4))
- : Real
5

REPLは値だけでなく型も表示してくれます
ちゃんと型チェックしてくれているか

> (distance 3 4)
Type Checker: type mismatch
  expected: pt
  given: Positive-Byte in: 3
Type Checker: type mismatch
  expected: pt
  given: Positive-Byte in: 4
Type Checker: Summary: 2 errors encountered in:
  3
  4

よしよし

2 Beginning Typed Racket

• #lang typed/racketはTyped Racketを使うよという宣言
• structには型修飾を付ける
• (-> pt pt Real)は関数の型
  • ->が関数のしるし
  • 最後の型(Real)が戻り値の型

関数自身を評価すれば関数自身の型も表示できます

> distance
- : (-> pt pt Real)
#<procedure:distance>

:print-typeも使えます

> (:print-type distance)
(-> pt pt Real)

こっちの方が表示はすっきり

2.1 Datatypes and Unions

• UはUnion型の定義
• define-typeで型に名前をつける

こう

(define-type Tree (U leaf node))
(struct leaf ([val : Number]))
(struct node ([left : Tree] [right : Tree]))

参照はこんな感じ
structで定義したときにleft-valやnode-leftも勝手に定義されています

(define t1 (node (leaf 1) (leaf 2)))
(leaf-val (node-left t1)) 

関数定義
組み込み型でも自分で定義した型でも書き方は同じ

(: tree-height (-> Tree Integer))
(define (tree-height t)
  (cond ((leaf? t) 1)
        (else (max (+ (tree-height (node-left t)) 1)
                   (+ (tree-height (node-right t)) 1)))))

(leaf? t)はtがleaf型かどうかを判定しています
これも勝手に定義されます

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (30)

いっぱい関数出てきたなと思いましてね
以前、Scheme手習いでインタプリタ作ったときに書いたような
関数の呼び出し関係の図を作ってみようと思ったんですけどね

たいへんな目に会いました

思ってたのを遥かに超えて複雑でした
うまく配置してみようという気も起こらないレベル

呼び出し関係図が複雑というのはどういうことを表しているんでしょうか

ひとつの数式に大量に情報がつめこまれているということになるのかな
関数の定義は1行でも、そのなかでいくつも関数が呼ばれてたりしますし
動かすためのコードとしてはありえない書き方がされてますが
ある意味100%関数型のプログラミングと言えなくもないですから
関数型の強みとも言えるかも

関数動詞の組み合わせの自由度が高いとも言えます
型がないですしね
証明も論理式も項もみんな数ですから

もちろんもともとの問題が複雑だということはあると思います
といっても、うまく設計すればここまで入り乱れることなく
いくつかのレイヤーに整理することはできそうな気も
ゲーデルさんがプログラムの保守性に気を使う言われはないですしね

前置記法に統一してたら楽だったでしょうか？
あんまりそんな気もしません

あと、Pは意外と呼ばれてないですね
端っこに追いやられてしまいました