如何消除衝突構造函數名稱

參見stdlib中的示例Data.Maybe.Base - 所有Maybe,Any和All都有一個just構造函數。如何消除衝突構造函數名稱

Agda允許這些定義。如何指定使用哪一個？

2017-09-13 M Farkas-Dyck

類型推斷。當你調用其中一個'just'函數時，它會嘗試查看你需要什麼樣的結果（根據你使用的結果）。如果這仍然不明確，你會得到一個錯誤，並且必須在某處添加一個明確的類型聲明。希望只有一個位於戰略位置，使所有其餘部分都清楚（但明確的類型聲明如果僅用於文檔，則總是很好的樣式）。 – Thilo

每種數據類型都有自己的模塊。所以Maybe,All和Any都是同時類型的構造函數和模塊。因此，您可以編寫Maybe.just,All.just或Any.just來消除構造函數的歧義。或者它可以通過類型推斷（統一是一個更合適的術語）或明確的類型簽名（如Thilo）在他們的評論中說明。（但是，如果存在一些不明確的地方，你會得到一個錯誤 - 你會得到一個未解決的問題）。

來源

2017-09-13 06:23:39 user3237465

如果你想獲得技術，最好的術語可能類似於「Type-directed disambiguation」，當你處於* checking *模式時可能會出現這種情況，因爲你已經有了一個類型，並且假設你希望表達式具有該類型，它很清楚構造函數對應的數據類型。 – gallais

@gallais，你可以通過統一獲得該類型。即如果你有'let f = just in f（fromMaybe 0（f 0））''，那麼即使我們可以進入推理模式，這兩個'f'也會被消歧。但是，是的，這類事情的正確術語是類型定向名稱解析。 – user3237465

你確實是對的。 – gallais

如何消除衝突構造函數名稱

回答

相關問題