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

html5 • • 问答

关于为什么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

编辑：添加了错误消息

回答

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具有多态类型，则可以两次评估昂贵的函数。

  • FWIW, the current GHC alpha has the new ImpredicativeTypes logic. Not sure if it will work in this particular case, but it will be available again soon.
以上是Haskell中的约束、函数组合和let抽象的全部内容。
THE END
分享
二维码
< <上一篇
下一篇>>