Typed Racket的類型推斷如何工作？

類型球拍做什麼樣的類型推斷？我發現拍郵件列表下面的代碼片段：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.

以上Blurb的使用術語「局部類型推理」，我還聽說「發生打字」用了很多，但我不完全確定這些術語的含義。

在我看來，類型球拍目前使用的類型推斷系統是不必要的弱。這是我的意思的一個例子。下列不類型檢查：

(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？這是球拍實施方式的一個基本限制（也就是說，由於球拍的某些更高級的類型特徵，這種推理實際上有時是錯誤的），或者這是將來可能實現的東西嗎？

來源

2012-10-24 Ord

山姆託賓艾施河畔赫希施塔特的博士論文應該有血淋淋的細節：http://www.ccs.neu.edu/racket/pubs/dissertation-tobin-hochstadt.pdf – dyoo

默認情況下，未註釋的頂層函數被假定爲輸入和輸出類型爲Any。我提供了這個模糊的解釋：因爲Racket的類型系統是，所以很靈活，它有時可以推斷出你不會期望的類型，並且允許某些程序在可能更喜歡它們發出類型錯誤時進行類型檢查。

切線：如果這適合您，也可以使用define:表格。

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

來源

2012-10-24 20:07:52

添加到這樣的回答：我會在一週中的任何一天採取「明確的」而不是「聰明的」。「聰明」的問題在於，作爲程序員，遲早你會在可檢查和不可檢查的邊界的另一邊結束，你必須弄清楚如何改變你的代碼檢查員可以驗證它。在這樣的情況下，試圖表明要吸引哪些聰明纔是非常困難的。 –

所以它聽起來好像沒有真正的基本*限制* - 相反，只是這種模糊的灰色區域是很好的類型和程序之間沒有的（也許這個區域在Typed Racket中比其他類型更大系統，因爲球拍系統非常靈活）。設計類型球拍推斷的人員儘可能遠離邊界儘可能遠離邊界：只有少數明確定義的情況可以進行類型推斷，其他所有事情都必須明確聲明。這樣，他們避免陷入混亂。這是對的嗎？ – Ord

@這就是對的。你可以閱讀山姆的博士論文的細節。他甚至將這一部分用於這個問題：3.2節。 –

Typed Racket的類型推斷如何工作？

回答

相關問題