1

我正在使用抽象语法树，我想给活页夹自己的类型。这似乎给 Idris 的整体检查带来了问题……

使用典型的自我参照TreeIdris 可以很好地进行整体检查。

data TreeShape = Last | More TreeShape TreeShape

Show TreeShape where
  show Last = "Leaf"
  show (More left right) = "Branch " ++ show left ++ " " ++ show right

同样与相互Tree：

mutual
  data MuTree = Another MuMuTree
  data MuMuTree = TheLeaf | TheBranch MuTree MuMuTree

  Show MuTree where
    show (Another x) = show x

  Show MuMuTree where
    show TheLeaf = "Leaf"
    show (TheBranch left right) = "Branch " ++ show left ++ " " ++ show right

但是，通过参数化提取的类型来引入间接性，并且整体检查失败：

data LeftBranch t = L t
(Show t) => Show (LeftBranch t) where
  show (L x) = show x
data TreeOutline = Final | Split (LeftBranch TreeOutline) TreeOutline

Show TreeOutline where
  show Final = "Leaf"
  show (Split left right) = "Branch " ++ show left ++ " " ++ show right

有没有办法让 Idris 正确检查最后一种递归类型的整体性？除此之外，除了在代码上撒上assert_totals 之外，还有什么其他的吗？

4

0 回答 0