代码之家 › 专栏 › 技术社区 › nicolas

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

haskell

nicolas · 技术社区 · 3 年前

为什么有一个简单的解释吗 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

编辑:添加错误消息

0 回复 | 直到 3 年前

chi 3 年前

Haskell的类型系统是表语 ,这意味着当我们使用多态值时 foo :: forall a . ... 类型系统只能实例化 a 单态( forall -免费)类型。

那么,为什么这些线条之间存在差异呢?

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

在第一种情况下,类型检查器能够检查 (unref_ok ...) ,将其结果推广到所需类型 (forall s. C s => Proxy s -> IO r) ,并将其传递给 compute_ok .

然而在第二种情况下, 计算机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目前不允许非专用性。这在未来可能会改变。

最后几点注意事项:

虽然我们不能实例化 b ~ forall ... ,我们可以实例化 b ~ T 哪里 newtype 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))

或者,另一种选择是禁用德雷德同态限制:

{-# LANGUAGE NoMonomorphismRestriction #-}

我不会重复DMR的精彩解释,可以在 this answer 简而言之,Haskell努力为非函数分配单态类型,例如 proxy_secret_s 因为在某些情况下,这可能会导致多次重新计算相同的值。例如。 let x = expensiveFunction y z in x + x 如果满足以下条件,则可以对昂贵的函数进行两次评估 x 具有多态类型。