kb84tkhrのブログ

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

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 boundB ... 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 ...だけでもわかるんじゃないの?

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

(: 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を消してやっても動くし
上の定義にしたがえば、これはCboundに対応して
関数の値の型がなくなってしまうはずなんだけどどうなってるの

(: 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をパラメータ化したもの、というだけしか書いてない

うーん