证明流的平等

Question

我有一个数据类型

data N a = N a [N a]

玫瑰树和应用实例

instance Applicative N where
 pure a = N a (repeat (pure a))
 (N f xs) <*> (N a ys) = N (f a) (zipWith (<*>) xs ys)

并需要证明适用法律.然而,纯粹创造无限深,无限分枝的树木.因此,例如,在证明同态定律

pure f <*> pure a = pure (f a)

我认为这证明了平等

zipWith (<*>) (repeat (pure f)) (repeat (pure a)) = repeat (pure (f a))

通过近似(或采取)引理将起作用.然而,我的尝试导致归纳步骤中的"恶性循环".特别是减少

approx (n + 1) (zipWith (<*>) (repeat (pure f)) (repeat (pure a))

给

(pure f <*> pure a) : approx n (repeat (pure (f a)))

其中approx是近似函数.如果没有明确的共同证据,我怎样才能证明这种平等？

Answer 1

以下是我认为有效并保持在程序语法和等式推理层面的一些内容的草图。

基本的直觉是，repeat x一般来说，推理比推理流（更糟糕的是列表）要容易得多。

uncons (repeat x) = (x, repeat x)

zipWithAp xss yss = 
    let (x,xs) = uncons xss
        (y,ys) = uncons yss
    in (x <*> y) : zipWithAp xs ys

-- provide arguments to zipWithAp
zipWithAp (repeat x) (repeat y) = 
    let (x',xs) = uncons (repeat x)
        (y',ys) = uncons (repeat y)
    in (x' <*> y') : zipWithAp xs ys

-- substitute definition of uncons...
zipWithAp (repeat x) (repeat y) = 
    let (x,repeat x) = uncons (repeat x)
        (y,repeat y) = uncons (repeat y)
    in (x <*> y) : zipWithAp (repeat x) (repeat y)

-- remove now extraneous let clause
zipWithAp (repeat x) (repeat y) = (x <*> y) : zipWithAp (repeat x) (repeat y)

-- unfold identity by one step
zipWithAp (repeat x) (repeat y) = (x <*> y) : (x <*> y) : zipWithAp (repeat x) (repeat y)

-- (co-)inductive step
zipWithAp (repeat x) (repeat y) = repeat (x <*> y)