idris - 在 where 子句中省略类型声明的条件

Question

tutorial where 子句部分给出了能够在 where 子句中省略函数 f 的类型声明的 2 个条件:

• f appears in the right hand side of the top level definition
• The type of f can be completely determined from its first application

我的问题是:这两个条件之间有什么关系？ 'and', 'or', 'mutually exclusive', 一个暗示另一个吗？

Answer 1

必须满足两个条件，例如:

test1 : List Int -> List Int
test1 xs = map inc xs
  where
    inc a = 1 + a

让我们看一下反例，其中只满足一个条件。

test2 : List Int -> List Int
test2 xs = map proxy xs
  where
    inc a = 1 + a
    proxy : Int -> Int
    proxy a = inc a

这里，inc没有出现在右边，但可以判断为Int -> Int。

test3 : List Int -> List Int
test3 xs = map (cast . inc . cast) xs
  where
    inc a = 1 + a

接下来，inc 出现在右侧，但无法确定类型(因为它可能是 Nat -> Nat，Int32 -> Int32 , …)，因此 cast 的类型也不能。

test2 和 test3 仅在给 inc 一个类型声明时编译。