基于 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

但是我无法在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中符号♯的绑定方式，这并没有帮助。

有人能想到一种方法来定义Idris中的左右识别器吗？我的P定义有误吗，还是我翻译函数的尝试有误？或者说Idris的全面性检查器还没有达到这种共归纳的水平？

- Vic Smith

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)

- oisdk

---

这个可以！我离开这个已经很久了，需要一点时间重新理解它，并弄清楚为什么它可以工作。我会在我做到之后接受的。 - Vic Smith