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 的类型系统是predicative，这意味着当我们使用多态值时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它不应用于参数，而是作为参数传递给 function (.)。代码真的意味着

(.) 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 不允许不可预测性。这在未来可能会改变。

最后几点说明：

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

• 原则上，预测性问题也适用于($) :: (a->b)->a->b算子。但是，在这种特定情况下，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 #-}

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