Idris

Question

假设我有以下内容

data Expr : Type -> Type where
  Lift : a -> Expr a
  Add  : Num a => Expr a -> Expr a -> Expr a
  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 ()

如果我在表达式树中上升一个级别，我想编写一个函数来重建 Zipper。类似于：

total
ZipUp : Zipper focus parent -> Type
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 ()

当我想将函数写入return a ZipUp

时，问题就来了

up : (x : Zipper focus parent) -> ZipUp x
up (Z e (R (Cnst l r) c x y)) = Z (Cnst l e) c
up (Z e (L (Cnst l r) c x y)) = Z (Cnst e r) c
up (Z e (R (Add l r) c x y))  = Z (Add l e) c
up (Z e (L (Add 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

这无法对 Add 案例进行类型检查，因为它无法推断 focus (type of e) 与 parent (expected type)

匹配

那么我的问题分为两部分。

我该怎么做才能表达这种关系？（如果 Zipper 是 R 构造的，则 e 与 r 具有相同类型，或者 e 与 [=22] 具有相同类型=] 在 L 构造的案例中。我尝试使用 {e = l} 和它的其他变体，但无济于事。）

如果我注释掉 up 的最后一行以结束：

，代码将进行类型检查并运行

up : (x : Zipper focus parent) -> ZipUp x
up (Z e (R (Cnst l r) c x y)) = Z (Cnst l e) c
up (Z e (L (Cnst l r) c x y)) = Z (Cnst e r) c

但是在 Add 的情况下，类型的实际操作应该是相同的，但是这无法进行类型检查，这是为什么？

感谢您花时间阅读and/or回答！

Answer 1

This fails to typecheck on the Add case, because it can't infer that focus (type of e) matches with parent (expected type)

因为情况并非总是如此，例如

*main> :t Z (Lift "a") (R (Add (Lift 1) (Lift 2)) Root (Lift 4) (Lift 8))
Z (Lift "a") (R (Add (Lift 1) (Lift 2)) Root (Lift 4) (Lift 8)) : Zipper String Integer

并且 Add (Lift 1) (Lift "a") 由于 Num a 约束而不起作用。

What can I do to express this relationship?

如果你想表达up内的关系：你有e : Expr f并且可以说在Add情况下应该使用相同的f：

up (Z {f} e (R (Add l r {a=f}) c x y)) = Z (Add l e) c
up (Z {f} e (L (Add l r {a=f}) c x y)) = Z (Add e r) c
up (Z e (R (Add l r) c x y)) = ?whattodo_1
up (Z e (L (Add l r) c x y)) = ?whattodo_2

由于 a != f 的情况，现在你有一个非总函数。我不太清楚您想做什么，所以我无法提供选择。 :-)

如果你想表达 Zipper 中的关系，你可以（非常粗略地）这样做：

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

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

现在，您在 R-Context 中构建一个 f = g 的拉链时构建一个证明。同样，我不能具体说明，但我希望它能以某种方式提供帮助。

Idris - 我可以表示模式匹配中的两个类型参数相等吗？

Idris - Can I express that two type parameters are equal in a pattern match?

equality

dependent-type

type-parameter