使用箭头作为原子值评估 AST（作为 GADT）

Question

以下程序进行类型检查并编译：

import Control.Arrow

data Ns = Na | Nb | Nc | Nd deriving Show

data Net a where
    Uni :: a -> Net a
    Serial :: Net a -> Net a -> Net a
    Branch :: Show a => Net a -> Net (Net a, Net a)

deriving instance Show a => Show (Net a)

eval :: (Arrow a) => Net c -> a b (Net c)
eval (Uni m) = arr (const (Uni m))
eval (Serial m n) = eval m >>> eval n
--eval (Branch m) = eval m &&& eval m

example = Serial (Serial (Uni Na) (Uni Nb)) (Serial (Uni Nc) (Uni Nd))

main = do
    putStrLn $ show (app (eval example, Na))

但是，当我尝试添加

eval (Branch m)

的情况时，请键入“检查炸弹”。有类型的东西

Arrow a => a b (Net d)

这是预料之中的，但当然我的方式是

Arrow a => a b (c',c'')

有人对如何写有建议吗

eval (Branch m)

？

编辑我

为了回应 @sabauma 评论，我认为

eval

的类型签名必须更改，但我不确定它应该是什么。

编辑二

以下是应该发生的情况的示例：

branch = Branch example
app (eval branch, Na)

应该给予，

Uni (Uni Na,Uni Na)

这就是@sabauma 的提案的作用。

Answer 1

一种可能性是

eval :: (Arrow a) => Net c -> a b (Net c)
eval (Uni m)      = arr (const (Uni m))
eval (Serial m n) = eval m >>> eval n
eval (Branch m)   = (eval m &&& eval m) >>> arr Uni

我不知道这是否具有所需的行为，但它会进行类型检查，但不是 简单的解决方案。这可以让您在不更改类型签名的情况下逃脱。

Answer 2

我的猜测是重新定义

Branch

以接受两个参数（因为 branching 在某种程度上意味着对我来说）：

data Net a where
  Uni :: a -> Net a
  Serial :: Net a -> Net a -> Net a
  Branch :: Show a => Net a -> Net a -> Net (Net a, Net a)

导致

eval :: (Arrow a) => Net c -> a b (Net c)
eval (Uni m) = arr (const $ Uni m)
eval (Serial m n) = eval m >>> eval n
eval (Branch l r) = (eval l) &&& (eval r) >>> arr (uncurry Branch)

但我不能说这个改变对你是否有意义。您可能应该给出一些解释如何使用您的类型。

Answer 3

虽然我不完全确定您的代码的目的，并且这可能不是您所追求的，但以下类型检查：

eval :: Arrow a => Net c -> a b (Net c)
eval (Uni m)      = arr (const (Uni m)) 
eval (Serial m n) = eval m >>> eval n
eval (Branch m)   = arr (const (Branch m)) 

当然，

arr . const

对于评估来说很有效，但现在我几乎肯定这不是你想要的。