free-theorem

11熱度

1回答

在伊德里斯，我能證明自由定理，例如'forall t'類型的唯一（全部）函數。 t - > t`是`id`？

對於充分多態的類型，參數可以唯一地確定函數本身（詳見Wadler's Theorems for free!）。例如，類型爲forall t. t -> t的唯一總功能是標識功能id。是否有可能在伊德里斯陳述和證明這一點？（如果它不能在伊德里斯內部證明，它是真的嗎？）以下是我的嘗試（我知道函數的相等不是伊德里斯的原始概念，所以我斷言泛型的任何函數t -> t總是返回相同的結果作爲身份函數將返回