haskell - 表征可以接受 `()` 作为输入的函数类型(不进行单态化)

Question

下面是几个简单的函数:

f1 :: () -> ()
f1 () = ()

f2 :: a -> a
f2 a = a

f3 :: a -> (a, a)
f3 a = (a, a)

f4 :: (a, b) -> a
f4 (a, b) = a

所有 f1 , f2 , 和 f3能够接受 ()作为输入。另一方面，当然， f4不能接受 () ; f4 ()是类型错误。
是否有可能从类型理论上描述 f1 , f2 , 和 f3有共同点？具体来说，是否可以定义 acceptsUnit函数，这样 acceptsUnit f1 , acceptsUnit f2 , 和 acceptsUnit f3类型正确，但 acceptsUnit f4是类型错误 - 并且没有其他影响？
以下内容完成了部分工作，但将其输入单态化(在 Haskell 中，我在 Hindley-Milner 中收集)，因此其效果不仅仅是断言其输入可以接受 () :

acceptsUnit :: (() -> a) -> (() -> a)
acceptsUnit = id

-- acceptsUnit f4     ~> error 😊
-- acceptsUnit f3 'a' ~> error ☹️

当然，同样的单态化也发生在下面。在这种情况下， acceptsUnit' 的注释类型是它的主要类型。

acceptsUnit' :: (() -> a) -> (() -> a)
acceptsUnit' f = let x = f () in f

Answer 1

f1 很容易从类型理论上描述什么, f2 , 和 f3但不是 f4有共同点。在 Hindley-Milner 的语言中，前三个具有可以专门化为以下形式的多型的多型:

forall a1...an. () -> tau

对于 n >= 0 和 tau 任意单型。第四个不行。
你能写一个接受前三个作为参数但拒绝第四个的函数吗？好吧，这取决于您使用的类型系统以及构建函数的范围。在通常的 Hindley-Milner 和/或标准 Haskell 类型系统中，如果您可以将候选函数的两个副本传递给接受函数，则以下内容将起作用:

acceptsUnit :: (() -> a) -> (b -> c) -> (b -> c)
acceptsUnit = flip const

f1 :: () -> ()
f1 () = ()

f2 :: a -> a
f2 a = a

f3 :: a -> (a, a)
f3 a = (a, a)

f4 :: (a, b) -> a
f4 (a, b) = a

main = do
  print $ acceptsUnit f1 f1 ()
  print $ acceptsUnit f2 f2 10
  print $ acceptsUnit f3 f3 10
  -- print $ acceptsUnit f4 f4  -- type error

这可能是您使用标准 Haskell 可以做到的最好的事情(并且可能是使用 Haskell 和 GHC 类型系统扩展可以做到的最好的事情，或者有人现在已经找到了一些东西)。
如果您可以使用自己的打字规则自由定义自己的打字系统，那么天空就是极限。