parsing - 基于 Agda 上的一篇论文在 Idris 中实现 Total Parser

Question

我正在尝试使用 Idris 实现总解析器，基于 this paper .首先，我尝试实现更基本的识别器类型 P :

Tok : Type
Tok = Char

mutual
  data P : Bool -> Type where
    fail : P False
    empty : P True
    sat : (Tok -> Bool) -> P False
    (<|>) : P n -> P m -> P (n || m)
    (.) : LazyP m n -> LazyP n m -> P (n && m)
    nonempty : P n -> P False
    cast : (n = m) -> P n -> P m

  LazyP : Bool -> Bool -> Type
  LazyP False n = Lazy (P n)
  LazyP True  n = P n

DelayP : P n -> LazyP b n
DelayP {b = False} x = Delay x
DelayP {b = True } x = x

ForceP : LazyP b n -> P n
ForceP {b = False} x = Force x
ForceP {b = True } x = x

Forced : LazyP b n -> Bool 
Forced {b = b} _ = b

这很好用，但我无法弄清楚如何从论文中定义第一个示例。在 Agda 是:

left-right : P false
left-right = ♯ left-right . ♯ left-right

但我不能让它在 idris 工作:

lr : P False
lr = (Delay lr . Delay lr)

生产

Can't unify 
    Lazy' t (P False)
with
    LazyP n m

如果你给它一些帮助，它会进行类型检查，如下所示:

lr : P False
lr = (the (LazyP False False) (Delay lr)) . (the (LazyP False False) (Delay lr))

但这被整体检查器拒绝，其他变体也是如此

lr : P False
lr = Delay (the (LazyP True False) lr) . (the (LazyP False False) (Delay lr))

我不完全确定 ♯运算符在 Agda 中绑定(bind)。

谁能看到在 Idris 中定义左右识别器的方法？是我对 P 的定义吗？错了，还是我试图翻译这个功能？还是 Idris 的整体检查器不完全符合这种共归纳法？

Answer 1

目前正在尝试自己移植这个库，似乎 Agda 向 Idris 推断出不同的隐含。这些是缺少的隐式:

%default total

mutual
  data P : Bool -> Type where
    Fail : P False
    Empty : P True
    Tok : Char -> P False
    (<|>) : P n -> P m -> P (n || m)
    (.) : {n,m: Bool} -> LazyP m n -> LazyP n m -> P (n && m)

  LazyP : Bool -> Bool -> Type
  LazyP False n = Inf (P n)
  LazyP True  n = P n

lr : P False
lr = (.) {n=False} {m=False} (Delay lr) (Delay lr)