1

我有以下内容：

data Expr : Type -> Type where
  Lift : a -> Expr a
  Add  : Num a => Expr a -> Expr a -> Expr a
  And  : Expr Bool -> Expr Bool -> Expr Bool
  Cnst : Expr a -> Expr b -> Expr a

data Context : Type -> Type where
  Root : Context ()
  L    : Expr w -> Context x -> Expr y -> Expr z -> Context w
  R    : Expr w -> Context x -> Expr y -> Expr z -> Context w 
  M    : Expr w -> Context x -> Expr y -> Expr z -> Context w 

data Zipper : Type -> Type -> Type where
  Z : Expr f -> Context g -> Zipper f g
  E : String -> Context g -> Zipper String ()



total
ZipUp : Zipper focus parent -> Type
ZipUp (Z e (R (And e1 e2) {x} c t u))      = Zipper Bool x
ZipUp (Z e (L (And e1 e2) {x} c t u))      = Zipper Bool x
ZipUp (Z e (R (Cnst {a} e1 e2) {x} c t u)) = Zipper a x
ZipUp (Z {f} e (L (Cnst l r) {x} c t u))   = Zipper f x
ZipUp (Z e (R (Add {a} e1 e2) {x} c t u))  = Zipper a x
ZipUp (Z {f} e (L (Add e1 e2) {x} c t u))  = Zipper f x
ZipUp _                                    = Zipper String ()

up : (x : Zipper focus parent) -> ZipUp x
up (Z e (R (And l r) c x y))  = Z (And l e) c
up (Z e (R (And l r) c x y))  = Z (And e r) c
up (Z {f = b} e (R (Cnst l {b} r) c x y)) = Z (Cnst l e) c
up (Z {f = a} e (L (Cnst l {a} r) c x y)) = Z (Cnst e r) c
up (Z {f = a} e (R (Add {a} l r) c x y))  = Z (Add l e) c
up (Z {f = a} e (L (Add {a} l r) c x y))  = Z (Add e r) c
up (Z e (R (Lift x) c l r))   = E "Some error" c
up (Z e (L (Lift x) c l r))   = E "Some error" c
up (E s c)                    = E s c

这不会对以下And情况进行类型检查，up因为 Idris 无法匹配我的问题是Zipper f g，Zipper Bool g我怎样才能让它工作，以便当我的表达式有具体类型的子级时我可以在树中重建一个级别？我认为我需要以某种方式改进类型，但我真的看不出制作新的依赖类型（或 GADT）将如何帮助解决这个问题（而且我不知道任何其他改进类型的方法！）

我已经查看了意见和证明，但是在尽力了几个星期之后，我似乎无法找到一种方法来编写问题来说出以下内容The focus of the zipper has the same type as the right child of the context's parent expression, if the context was constructed with R. The same is true for the focus and the context's left child, if the context was constructed with L.

我尝试增加类型参数，以便每个表达式都包含其子项的类型，Expr a l m r但我最终会遇到相同的错误，即使我可以编写一个新版本来R : Expr r t u v -> Expr a l m r -> Expr m h i j -> Expr r x y z -> Context -> Context捕获这种关系。最后，我需要一种方法来告诉 Idris 某些参数a确实Bool处于某种模式匹配之下！

我非常卡住，所以任何建议都会非常感激！

亲切的问候，多诺万

4

1 回答 1

1

当然，这些构造函数的类型不够精确：w、x、y和之间没有联系z。

L    : Expr w -> Context x -> Expr y -> Expr z -> Context w
R    : Expr w -> Context x -> Expr y -> Expr z -> Context w 
M    : Expr w -> Context x -> Expr y -> Expr z -> Context w
于 2018-02-09T16:21:14.307 回答