kb84tkhrのブログ

何を書こうか考え中です あ、あと組織とは関係ないってやつです 個人的なやつ

Typed Racketのお勉強 (4)

racket

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型ということにされてしまいました