14

Typed Racketはどのような型推論を行いますか？Racketメーリングリストで次のスニペットを見つけました。

Typed Racket型システムには、Hindley / Milnerスタイルの型システムでサポートされている機能を超える多くの機能が含まれているため、その推論システムを使用することはできません。現在、Typed Racketはローカル型推論を使用してプログラム内の多くの型を推論していますが、さらに多くの型を推論したいと考えています。これは現在進行中の研究分野です。

上記の宣伝文句は「ローカル型推論」という用語を使用しており、「オカレンスタイピング」もよく使用されていると聞きましたが、これらの用語が何を意味するのか正確にはわかりません。

TypedRacketが現在使用している型推論システムは不必要に弱いように思えます。これが私の言いたいことの例です。以下はタイプチェックではありません：

(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を付ける必要があります。(: midpoint (pt pt -> pt))そうしないと、次のエラーが発生しますType Checker: Expected pt, but got Any in: p1。なぜタイプチェッカーは、これからタイプp1とがそうであるp2 必要があると結論付けることができないのptですか？これは、Racketが型を実装する方法の根本的な制限ですか（つまり、Racketのより高度な型機能のいくつかのために、この推論の行が実際に間違っている場合があります）、またはこれは将来実装される可能性がありますか？

4

1 に答える 1

6

デフォルトでは、注釈のないトップレベル関数は、入力タイプと出力タイプが。であると想定されていますAny。この漠然とした説明を提供します。Racketの型システムは非常に柔軟であるため、予期しない型を推測したり、一部のプログラムで型エラーを出力したいときに型チェックを実行したりできる場合があります。

接線：それがあなたにdefine:合っている場合は、フォームを使用することもできます。

(define: (midpoint [p1 : pt] [p2 : pt]) : pt
  ...)
于 2012-10-24T20:07:52.797 に答える