haskell - Haskell 中的约束、函数组合和 let 抽象

Question

是否有一个简单的解释为什么ko1和 ko2失败 ？

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module SOQuestionExistential where

import Data.Proxy

------------------------------------------------------------------------------

class C s where
  important_stuff :: proxy s -> a

compute_ok :: forall r. (forall s. C s => Proxy s -> IO r) -> IO r
compute_ok k = undefined

unref_ok :: Proxy s -> Proxy s -> IO ()
unref_ok _ _ = return ()

----

ok :: (forall s. C s => t -> Proxy s) -> t -> IO ()
ok calc t = compute_ok (unref_ok (calc t))

ko1 :: (forall s. C s => t -> Proxy s) -> t -> IO ()
ko1 calc t = (compute_ok . unref_ok) (calc t)

-- • Couldn't match type ‘s’ with ‘s0’
--   ‘s’ is a rigid type variable bound by
--     a type expected by the context:
--       forall s. C s => Proxy s -> IO ()

ok' :: (forall s. C s => t -> Proxy s) -> t -> IO ()
ok' calc t = compute_ok (unref_ok (let proxy_secret_s = calc t in proxy_secret_s))

ko2 :: (forall s. C s => t -> Proxy s) -> t -> IO ()
ko2 calc t = let proxy_secret_s = calc t in compute_ok (unref_ok (proxy_secret_s))


-- • No instance for (C s1) arising from a use of ‘calc’
-- • In the expression: calc t
--   In an equation for ‘proxy_secret_s’: proxy_secret_s = calc t
--   In the expression:
--     let proxy_secret_s = calc t
--     in compute_ok (unref_ok (proxy_secret_s))typec

编辑:添加了错误消息

Answer 1

Haskell 的类型系统是谓词系统，这意味着当我们使用多态值 foo :: forall a . ... 时类型系统只能实例化 a具有单态( forall -free)类型。
那么，为什么这些行之间存在差异？

compute_ok (unref_ok ...)
(compute_ok . unref_ok) ...

在第一个中，类型检查器可以检查 (unref_ok ...) ，将其结果推广到所需的类型 (forall s. C s => Proxy s -> IO r) ，并将其传递给 compute_ok .
然而，在第二种情况下，compute_ok不应用于参数，而是作为参数传递给函数 (.) .代码真的意味着

(.) compute_ok unref_ok ...

现在，函数的类型是什么(.) ?

(.) :: (b->c) -> (a->b) -> (a->c)

使(compute_ok . unref_ok)我们需要选择的工作 b ~ (forall s. C s => Proxy s -> IO r)但是，唉，这是一种多态类型，并且预测性禁止对 b 进行这种选择。 .
GHC 开发人员已经提出了几次尝试使 Haskell “减少预测性”并允许某些类型的不可预测性。其中一个甚至已作为扩展实现，然后实际上已弃用，因为它与其他几个扩展不能很好地配合使用。所以，事实上，此时的 Haskell 不允许不可预测性。这在 future 可能会改变。
最后几点说明:

虽然我们不能实例化 b ~ forall ... ，我们可以实例化 b ~ T哪里newtype T = T (forall ...)因为这由类型系统处理得很好。当然，使用它需要包装/解包，这不是那么方便，但原则上它是一种选择。

原则上，预测性问题也适用于 ($) :: (a->b)->a->b运算符(operator)。但是，在这种特定情况下，GHC 开发人员决定使用临时解决方案修补类型系统:f $ x类型检查为 f x ，允许 f采取多态输入。这种特殊情况不会扩展到 . :f . g . h $ x未类型检查为 f (g (h x))这将在发布的代码中节省一天。

第二个例子可以通过给 proxy_secret_s 一个显式的多态签名来修复。 .

ko2 :: (forall s. C s => t -> Proxy s) -> t -> IO ()
ko2 calc t = let 
   proxy_secret_s :: forall s. C s => Proxy s
   proxy_secret_s = calc t 
   in compute_ok (unref_ok (proxy_secret_s))

或者，禁用 Dreaded Monomorphism Restriction:

{-# LANGUAGE NoMonomorphismRestriction #-}

我不会重复可以在 this answer 中找到的对 DMR 的出色解释。 .简而言之，Haskell 尝试将单态类型分配给非函数，例如 proxy_secret_s因为在某些情况下可能会导致多次重新计算相同的值。例如。 let x = expensiveFunction y z in x + x如果 x，可以对昂贵的函数求值两次有一个多态类型。