haskell – 有什么方法可以快速确定为函数提供多少个类型的孔？

2023年3月13日 247次阅读

Typed holes提供了一种很好的方法来找到如何实现的东西：如果你知道要使用什么函数,比如foo,你可以写出类似foo _ _ _的东西,让编译器告诉你每个参数的预期类型.这使得查找任何文档几乎没有必要.

但是,只有在实际写出正确数量的下划线时,它才能正常工作.目前,我通常通过一些试错来确定这一点,但是并不总是很明显需要注意什么提示,因为在Haskell函数中总是可以部分应用.

什么是尽快找出这个数字的好方法？

最佳答案 正如@chi建议的那样,我发现的最好的事情是“将洞应用到函数中”.我不知道这是否回答了这个问题,但希望它至少在某种程度上有所帮助.

我猜通过“函数总是可以部分应用”你的意思是你可以有这样的功能：

foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
foldr = undefined

你无法从类型中分辨出为了在任何特定类型进行类型检查需要多少参数.类型检查员在这里可以做的最好的事情是告诉你它接受的最小参数数量：

bar :: String -> String
bar = _1 foldr

* Found hole:
    _1 :: ((a0 -> b0 -> b0) -> b0 -> t0 a0 -> b0) -> String -> String
  Where: `t0' is an ambiguous type variable
         `b0' is an ambiguous type variable
         `a0' is an ambiguous type variable
* In the expression: _
  In the expression: _ foldr
  In an equation for `bar': bar = _ foldr

* Ambiguous type variable `t0' arising from a use of `foldr'
  prevents the constraint `(Foldable t0)' from being solved.
  Probable fix: use a type annotation to specify what `t0' should be.
  These potential instances exist:
    instance Foldable (Either a) -- Defined in `Data.Foldable'
    instance Foldable Maybe -- Defined in `Data.Foldable'
    instance Foldable ((,) a) -- Defined in `Data.Foldable'
    ...plus one other
    ...plus 22 instances involving out-of-scope types
    (use -fprint-potential-instances to see them all)

旁白：第二个错误在这里不是特别有用,因为t0可能真的是这些类型中的任何一个.但是如果你经常发现自己处于这种情况,那么-fprint-potential-instances可能实际上是有用的.

你现在可以在头脑中做一些类型的检查：

((a0 -> b0 -> b0) ->  b0  -> t0 a0  -> b0     ) -> 
  <_1>               <_2>    String -> String

要匹配的类型,您必须至少提供两个孔.您可能需要更多,但这将取决于b0的实例化.替换这些漏洞,你会遇到一个非常简单的问题

bar :: String -> String
bar = foldr _1 _2

* Found hole: _1 :: Char -> String -> String

* Found hole: _2 :: String

你甚至可能会遇到(在我看来,愚蠢)的功能

class C a where foo :: a
instance C String where
instance C a => C (Int -> a) where

在这种情况下,您可以执行相同的操作,并且typechecker可以帮助您通知所有可能的实例：

bar :: String -> String
bar = _ foo

test0.hs:6:7: warning: [-Wtyped-holes]
    * Found hole: _ :: t0 -> String -> String
      Where: `t0' is an ambiguous type variable
    * In the expression: _
      In the expression: _ foo
      In an equation for `bar': bar = _ foo
    * Relevant bindings include
        bar :: String -> String (bound at test0.hs:6:1)

test0.hs:6:9: warning: [-Wdeferred-type-errors]
    * Ambiguous type variable `t0' arising from a use of `foo'
      prevents the constraint `(C t0)' from being solved.
      Probable fix: use a type annotation to specify what `t0' should be.
      These potential instances exist:
        instance C a => C (Int -> a) -- Defined at test0.hs:3:10
        instance C String -- Defined at test0.hs:2:10
    * In the first argument of `_', namely `foo'
      In the expression: _ foo
      In an equation for `bar': bar = _ foo

在这里你真的要猜.在这个(公认的做作的)例子中,我可能猜测你想要一个参数,因为bar需要一个参数.

bar :: String -> String
bar = foo . _

test0.hs:6:7: warning: [-Wdeferred-type-errors]
    * Ambiguous type variable `b0' arising from a use of `foo'
      prevents the constraint `(C (b0 -> String))' from being solved.
        (maybe you haven't applied a function to enough arguments?)
      Probable fix: use a type annotation to specify what `b0' should be.
      These potential instance exist:
        instance C a => C (Int -> a) -- Defined at test0.hs:3:10

test0.hs:6:13: warning: [-Wtyped-holes]
    * Found hole: _ :: String -> b0
      Where: `b0' is an ambiguous type variable

现在它告诉你有一个潜在的实例,所以你可以猜到那个洞的类型真的应该是String – >诠释.

点赞