4

是否可以为包含“空白”的 Haskell 值提供类型签名以供类型推断算法填充？

非常人为的上下文示例：

m = return ('I', (("don't", "really"), "care", ["what", "this"], "type"), "is") 

b = isJust m

这行得通。isJust min的使用b限制了mto be的类型Maybe <something>，而m's 的定义限制了mto be的类型<something> (Char, ((String, String), String, [String], String), String)，编译器将这两条信息放在一起计算出精确的类型m。

但是假设我没有对 应用任何Maybe特定函数m，所以我需要一个手动类型签名来停止return多态。我不能这样说：

m :: Maybe a
m = return ('I', (("don't", "really"), "care", ["what", "this"], "type"), "is")

因为那是不正确的。类型并不Maybe a适用于所有a，它Maybe a适用于a我希望编译器推断的一些；程序中有足够的信息供编译器执行此操作，从我的第一个示例中我们可以看到，编译器能够将多个约束放在一起，其中没有单独的约束足以确定类型是什么，但是它们一起完全指定了类型。

我想要的是能够给出类似的类型m :: Maybe _，其中的_意思是“你弄清楚这里发生了什么”，而不是像m :: Maybe a.

有什么办法可以说这样的话吗？我可以看到的替代方案是明确给出完整类型：

m :: Maybe (Char, ((String, String), String, [String], String), String)
m = return ('I', (("don't", "really"), "care", ["what", "this"], "type"), "is")

或者给表达式的一部分一个类型签名，它具有约束Maybe类型签名的一部分而不是约束的效果a，例如：

m = (return :: a -> Maybe a) ('I', (("don't", "really"), "care", ["what", "this"], "type"), "is")

或者在m没有显式类型签名的情况下离开并引入未使用的额外定义来约束m：

m = return ('I', (("don't", "really"), "care", ["what", "this"], "type"), "is") 

b = isJust m

或者直接使用单态函数：

m = Just ('I', (("don't", "really"), "care", ["what", "this"], "type"), "is")

显然，这不是特定于Maybe，也不是* -> *类型构造函数的参数；我可以想象想说“这个值是一个单子，对于Int某些单子”而不想说“这个值是任何单子的单子”，或者“这是一个来自其他类型的函数”而不是说“这是一个功能从任何其他类型`。IntIntInt

我最感兴趣的是是否有什么东西可以让我相当直接地声明像上面关于值的声明，出于可读性目的，而不是难以阅读的变通方法（比如为return. 我知道，如果我的目标是简单地将额外的类型信息输入编译器以将其关闭关于模棱两可的类型变量，那么有无数种方法可以做到这一点。

4

4 回答 4

6

不幸的是，GHC 不允许您直接指定部分签名，尽管这样会很棒。

在这种情况下，做你想做的事情的一种方法是m = return ... `asTypeOf` (undefined :: Maybe a)，其中asTypeOf是一个 Prelude 函数:: a -> a -> a，它返回它的第一个参数但强制它与第二个参数统一。

这是你在评论中提出的一个很好的观点——undefined :: SomeType让我也很难过。这是另一个解决方案：

import Data.Proxy

proxiedAs :: a -> Proxy a -> a
proxiedAs = const

现在你可以说m = return ... `proxiedAs` (Proxy :: Proxy (Maybe a))，并且看不到 ⊥。

于 2012-12-07T07:31:08.183 回答
5

你可以这样写：

asMaybe :: Maybe a -> Maybe a
asMaybe = id

m = asMaybe $ return ('I', (("don't", "really"), "care", ["what", "this"], "type"), "is")

我在classy-prelude、提供asByteString、asSet、asList等中使用了这种技巧。

于 2012-12-07T07:28:59.307 回答
3

在 GHC 7.10 中，现在有了 PartialTypeSignatures扩展，它完全启用了我在问题中编写的假设下划线语法。来自上面链接的文档页面的示例：

not' :: Bool -> _
not' x = not x
-- Inferred: Bool -> Bool

maybools :: _
maybools = Just [True]
-- Inferred: Maybe [Bool]

just1 :: _ Int
just1 = Just 1
-- Inferred: Maybe Int

filterInt :: _ -> _ -> [Int]
filterInt = filter -- has type forall a. (a -> Bool) -> [a] -> [a]
-- Inferred: (Int -> Bool) -> [Int] -> [Int]

仅使用PartialTypeSignatures扩展名，编译器就会发出带有推断类型的警告，以防它们只是您打算在最终版本之前填写的占位符。通过添加-fno-warn-partial-type-signatures标志，您可以告诉它您打算保留部分签名。

于 2016-02-09T10:32:41.067 回答
1

从 Michael Snoyman 的建议中综合一下，如果我：

  1. 不想为我想做的每个类型断言定义一个特定的函数
  2. 想要真正写出接近我所做类型断言的类型
  3. 不想写两次类型

我可以做类似的事情：

type Assert a = a -> a

m = (id :: Assert (Maybe a)) $ return ('I', (("don't", "really"), "care", ["what", "this"], "type"), "is")
于 2012-12-07T07:49:07.223 回答