方法(改进？是吗？)将类型变量转换为Idris中的具体类型？对于依赖类型的HOAS Zipper

Question

我有以下几点：

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 

这不会对up的And用例进行类型检查，因为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的！

我被困住了，所以任何建议都将不胜感激！

致以亲切的问候，多诺万

Answer 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