型付きラケットの型推論はどのように機能しますか？

Question

Typed Racketはどんなタイプの推論をしますか？私は、ラケットのメーリングリスト上で次のスニペットが見つかりました：

The Typed Racket type system contains a number of features that go beyond what's supported in Hindley/Milner style type systems, and so we can't use that inference system. Currently, Typed Racket uses local type inference to infer many of the types in your program, but we'd like to infer more of them -- this is an ongoing area of research.

を上記の宣伝文句は、「ローカル型推論」という用語を使用し、私も聞いた「発生タイピング」多くを使用しますが、私は正確ではありませんよこれらの用語が何を意味するか。

Typed Racketが現在使用している型推論システムは不必要に弱いと思われます。ここに私が意味するものの例があります。以下は型チェックしません：

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

(define (midpoint p1 p2) 
    (pt (/ (+ (pt-x p1) (pt-x p2)) 2) 
     (/ (+ (pt-y p1) (pt-y p2)) 2))) 

あなたが明示的に(: midpoint (pt pt -> pt))でmidpointに注釈を付ける必要があり、そうでなければ、エラーを取得：Type Checker: Expected pt, but got Any in: p1を。タイプチェッカーでは、p1とp2のタイプがの場合はptであると結論づけることはできません。これは、ラケットがタイプを実装する方法の根本的な制限ですか（つまり、ラケットのより高度なタイプの機能のために、実際にが間違ってのこのラインです）、またはこれは将来実現される可能性がありますか？

Answer 1

既定では、注釈なしのトップレベル関数は入力と出力の型がAnyであると見なされます。私はこのあいまいな説明を提供しています：ラケットタイプのシステムはですので、柔軟性があります。あなたが予想しないタイプを推測することがあり、タイプエラーを出すことを望むときにタイプチェックを行うプログラムがあります。

タンジェント：define:フォームを使用することもできます。サム・トービン-ホックシタットの博士論文は、血みどろの詳細を持っている必要があり

(define: (midpoint [p1 : pt] [p2 : pt]) : pt 
    ...)