你能在哈斯克尔中部分约束一个类型吗?



是否可以为包含"空白"的Haskell值提供类型签名,以便类型推断算法填写?

非常人为的上下文示例:

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

这行得通。isJust mb中的使用限制了要Maybe <something>m类型,而m的定义限制了要<something> (Char, ((String, String), String, [String], String), String)m类型,编译器将这两个信息放在一起,以计算出精确的m类型。

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

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

因为这是不正确的。该类型并非对所有aMaybe a,对于我希望编译器推断的某些aMaybe 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,对于某个monad",而不想说"这个值是任何monad的一元Int",或者"这是一个从Int到其他类型的函数"而不说"这是一个从Int任何其他类型的函数"。

我最感兴趣的是是否有一些东西允许我相当直接地陈述上面关于值的声明,出于可读性目的,而不是难以阅读的解决方法(例如为return提供显式类型签名)。我知道,如果我的目标只是简单地将额外的键入信息放入编译器以关闭关于模棱两可的类型变量,那么有无数种方法可以做到这一点。

不幸的是,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)),看不到⊥。

你可以这样写:

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

我在经典前奏中使用这种技巧,提供asByteStringasSetasList等。

在 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标志,您可以告诉它您打算保留部分签名。

从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")

最新更新