Haskell：從類型

中扣除函數所以我今天在玩Haskell，考慮給定類型的函數定義的自動生成。Haskell：從類型

例如，函數

twoply :: (a -> b, a -> c) -> a -> (b, c)

是明顯，我給出的類型（如果我排除使用undefined :: a）的定義。

於是我想出了以下內容：

¢ :: a -> (a ->b) -> b 
¢ = flip ($)

其具有

(¢) ¢ ($) :: a -> (a -> b) -> b

這讓我想起了我的問題的有趣的屬性。鑑於與「具有相同類型」的關係=::=，陳述x =::= x x ($)是否唯一定義了x的類型？必須x =::= ¢，還是存在x另一種可能的類型？

我試過從x =::= x x ($)後退工作推斷x :: a -> (a -> b) -> b，但陷入困境。

2010-09-16 rampion

sepp2k回答了你的問題，但值得注意的是'flip id'是你的''''的一個等價定義，使得你注意到的屬性的原因更加明顯（至少對我而言）。 – 2010-09-17 00:11:12

這是古怪而可怕的 – rampion 2010-09-17 00:46:32

換句話說，冒着過度解釋它的風險，專用於函數的'id :: a - > a'相當於'（$）::（a - > b） - >（ a - > b）'。多態不是很好嗎？ – 2010-09-17 21:12:34

x =::= x x ($)對x = const也是如此，其類型爲a -> b -> a。所以它不能唯一標識類型。

2010-09-16 23:08:27 sepp2k

從上面的等式中，我們可以確定x的一些類型簽名。 X不需要這種類型，但至少需要統一這種類型。

$ :: forall a b. (a -> b) -> a -> b 
x :: t1 -> ((a -> b) -> a -> b) -> t1

鑑於此，應該很簡單地編寫x的大量實現。

2010-09-17 00:25:12 sclv

我只想補充一點，你應該看看http://hackage.haskell.org/package/djinn。它可以採用許多類型簽名並從中派生出一個實現。如果djinn可以理解的類型只有一個可能的實現，它就會生成它。

2010-09-17 04:40:42 Carl

回答