在 Idris 中证明流函数的性质

Question

我正在尝试证明有关流函数和 Monadic Stream Functions [1]（最终是 FRP 程序）的属性。

Idris 对我对流函数的形式化感到满意：

module SF

import Data.Vect
import Syntax.PreorderReasoning

%default total

data SF : Type -> Type -> Type where
  SFG : (a -> (b, Inf (SF a b))) -> SF a b

steps : {n : Nat} -> SF a b -> Vect n a -> Vect n b
steps {n = Z}   (SFG s) []        = []
steps {n = S m} (SFG s) (a :: as) =
    let (b, s') = s a
        bs = steps s' as
    in (b::bs)

我可以简单地定义提升/逐点应用函数：

liftM : (a -> b) -> SF a b
liftM f = SFG $ \a => (f a, liftM f)

以及 SF 身份的两种变体：

identityM : SF a a
identityM = SFG $ \a => (a, identityM)

identity2 : SF a a
identity2 = liftM id

这通过了 Idris 的整体检查器。但是，如果我现在尝试证明 identityM 和 identity2 相等，我就会遇到问题。我可以如下声明该属性：

proof1 :  (Eq b)
       => (n : Nat)
       -> (v : Vect n a)
       -> (steps identityM v) = (steps identity2 v)
proof1 Z [] = ?proof1_rhs_1
proof1 (S k) v = ?proof1_rhs_2

如果我询问?proof1_rhs_1 的类型，idris 正确地说是steps identityM [] = steps identity2 []。但是，如果我尝试使用等式推理来表达这一点：

proof1 Z [] = (steps {n=Z} identityM []) ={ ?someR }=
              (steps {n=Z} identity2 []) QED

然后idris不高兴了：

When checking argument x to function Syntax.PreorderReasoning.Equal.qed:
        Type mismatch between
                steps identity2 [] (Inferred value)
        and
                steps identity2 [] (Given value)

        Specifically:
                Type mismatch between
                        steps identity2
                and
                        []Unification failure

有什么办法可以做到吗？

[1]https://dl.acm.org/citation.cfm?id=2976010

Answer 1

这是通常的“Idris 的隐式概括导致混淆范围规则”：

proof1 :  (Eq b)
       => (n : Nat)
       -> (v : Vect n a)
       -> (steps identityM v) = (steps identity2 v)

意思

proof1 : {identityM : _} -> {identity2 : _} -> (...)
       -> (steps identityM v) = (steps identity2 v)

要引用前面的定义，您需要使用限定名称SF.identityM 和SF.identity2。您可能还有其他问题（Eq b 和 b 在其他类型的其他地方都没有提到似乎可疑）。