基于Agda论文在Idris中实现总分析器

Question

我正在尝试使用Idris实现总解析器,基于本文.首先,我尝试实现更基本的识别器类型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

但我不能让这个在伊德里斯工作:

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中绑定,这没有任何帮助.

任何人都可以看到在伊德里斯定义左右识别器的方法吗？我的P错误定义,还是我试图翻译这个功能？或者伊德里斯的整体检查是不是完全没有这个coinductive的东西？

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)