为什么不这个类型检查呢？

Question

这是玩具示例.s:

{-# LANGUAGE ImpredicativeTypes #-}

import Control.Arrow

data From = From (forall a. Arrow a => a Int Char -> a [Int] String)

data Fine = Fine (forall a. Arrow a => a Int Char -> a () String)

data Broken = Broken (Maybe (forall a. Arrow a => a Int Char -> a () String))

fine :: From -> Fine
fine (From f) = Fine g
  where g :: forall a. Arrow a => a Int Char -> a () String
        g x = f x <<< arr (const [1..5])

broken :: From -> Broken
broken (From f) = Broken (Just g) -- line 17
  where g :: forall a. Arrow a => a Int Char -> a () String
        g x = f x <<< arr (const [1..5])

这就是ghci的想法:

GHCi, version 7.0.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Loading package ffi-1.0 ... linking ... done.
Prelude> :l toy-example.hs 
[1 of 1] Compiling Main             ( toy-example.hs, interpreted )

toy-example.hs:17:32:
    Couldn't match expected type `forall (a :: * -> * -> *).
                                  Arrow a =>
                                  a Int Char -> a () String'
                with actual type `a0 Int Char -> a0 () String'
    In the first argument of `Just', namely `g'
    In the first argument of `Broken', namely `(Just g)'
    In the expression: Broken (Just g)
Failed, modules loaded: none.

为什么fine类型检查,同时broken不？

我如何进入类型检查broken？

(在我的实际代码中a,Broken如果必须的话,我可以添加类型参数,而不是在构造函数中对它进行普遍量化,但是如果可能的话我想避免这种情况.)

---

编辑:如果我改变的定义Broken来

data Broken = Broken (forall a. Arrow a => Maybe (a Int Char -> a () String))

然后是brokentypechecks.好极了!

但是,如果我然后添加以下功能

munge :: Broken -> String
munge (Broken Nothing) = "something"  -- line 23
munge (Broken (Just f)) = f chr ()

然后我收到错误信息

toy-example.hs:23:15:
    Ambiguous type variable `a0' in the constraint:
      (Arrow a0) arising from a pattern
    Probable fix: add a type signature that fixes these type variable(s)
    In the pattern: Nothing
    In the pattern: Broken Nothing
    In an equation for `munge': munge (Broken Nothing) = "something"

我怎么munge去typecheck？

第二编辑:在我的真正的程序我已经取代了Broken (Maybe ...)构造函数BrokenNothing和BrokenJust ...构造函数(已经有其他的构造函数),但我很好奇的模式匹配应该是怎样在这种情况下工作.

Answer 1

ImpredicativeTypes无论如何，GHC 版本之间的变化都会让你处于相当不稳定的境地 - 他们正在努力寻找一种能够适当平衡功能、易用性和易于实现的预测性表述。

在这种特殊情况下，尝试将量化类型放入 a 中Maybe（这是一种未明确定义为以这种方式运行的数据类型）确实很棘手，因此我建议像您提到的那样使用自定义构造函数。

我认为您可以munge通过重新解构BrokenRHS 上的参数来修复上述问题，此时其所使用的类型将是已知的，例如：

munge (Broken x@(Just _)) = fromJust x chr ()

不过，它非常丑陋。