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

回答