Idris

Question

当我尝试在 REPL 中使用依赖类型的函数时，我在 Idris 中遇到了意外类型错误的问题。这是我拥有的：

data Expr : Type -> Type where
  Null     : Expr ()
  Lift     : Show a => a -> Expr a
  Add      : Num a => Expr a -> Expr a -> Expr a
  Mul      : Num a => Expr a -> Expr a -> Expr a

data Context : Type where
  Root  : Context
  Error : String -> Context
  L     : Expr a -> Context -> Expr b -> Expr c -> Context
  R     : Expr a -> Context -> Expr b -> Expr c -> Context
  M     : Expr a -> Context -> Expr b -> Expr c -> Context

data Zipper : Type -> Type where
  Z : Expr a -> Context -> Zipper a
  E : String -> Context -> Zipper String

UnZip : Zipper b -> Type
UnZip (Z {a} e c) = Expr a
UnZip (E x c)     = String

unZip : (x : Zipper a) -> UnZip x
unZip (Z e c) = e
unZip (E x c) = x

total
ZipRight : Zipper a -> Type
ZipRight (Z (Add {a} l r) c)            = Zipper a
ZipRight (Z (Mul {a} l r) c)            = Zipper a
ZipRight _                              = Zipper String

err : String
err = "Some Error"

total
right : (x : Zipper a) -> ZipRight x
right (Z Null c)                     = E err c
right (Z (Lift _) c)                 = E err c
right (Z (Add l r) c)                = Z r (R (Add l r) c Null l)
right (Z (Mul l r) c)                = Z r (R (Mul l r) c Null l)

当我转到运行 REPL 中的以下内容时 unZip $ right $ Z (Add (Lift 2) (Mul (Lift 3) (Lift 4))) Root 我得到了预期的 Expr Integer.

当我在行中添加额外的 right unZip $ right $ right $ Z (Add (Lift 2) (Mul (Lift 3) (Lift 4))) Root 我在 ZipRight (right (Z (Add (Lift 2) (Sub (Lift 4) (Lift 5))) Root)) (Type of right (right (Z (Add (Lift 2) (Sub (Lift 4) (Lift 5))) Root))) 和 Zipper a (Expected Type)

之间收到类型错误

然而运行ning right $ right $ Z (Add (Lift 2) (Mul (Lift 3) (Lift 4))) Root 显示预期的 Zipper Integer.

我想知道的是。为什么我在第二次调用 right 时遇到类型错误，有没有办法修复我的代码，这样错误就不会再发生，或者我可以重构问题的方式被规避了？

亲切的问候，

多诺万

Answer 1

使函数合计解决了这个问题。至于为什么问题首先出现，我还是一头雾水！

Idris - 依赖类型函数中的类型错误

Idris - Type errors in dependently typed functions

functional-programming

dependent-type