wrapper - 我可以为表示包装其他类型的类型的 Wrapper 接口(interface)编写通用函数包装函数吗？

Question

下面的完整代码示例(已成功编译)是我的问题的简化且稍微做作的示例。

NatPair 是一对 Nat ，我想使用函数 Num 将二进制 NatPair 操作逐点“提升”到 lift_binary_op_to_pair 。

但我无法实现 Num NatPair，因为 NatPair 不是数据构造函数。

因此，我将其包装在类型 WrappedNatPair 中，并且我可以为该类型提供 Num 实现，以及相应的“提升”版本 + 和 * 。

然后我想用我的 Wrapper 接口(interface)概括包装类型的想法。

函数lift_natpair_bin_op_to_wrapped可以从NatPair开始进行二进制运算到 WrappedNatPair ，实现代码完全是根据 unwrap 和 wrap Wrapper 接口(interface)方法。

但是，如果我尝试概括为

lift_bin_op_to_wrapped : Wrapper t => BinaryOp WrappedType -> BinaryOp t

那么类型签名甚至无法编译，并出现错误:

 `-- Wrapping.idr line 72 col 23:
     When checking type of Main.lift_bin_op_to_wrapped:
     Can't find implementation for Wrapper t

(其中错误位置是类型签名中“:”的位置)。

我认为问题是 t 没有出现在Wrapper 接口(interface) WrapperType 方法的类型签名，所以 WrapperType 不能在内部以外的任何地方调用接口(interface)定义本身。

(解决方法是每次都使用相同的实现代码 lift_<wrapped>_bin_op_to_<wrapper> 编写样板 op x y = wrap $ op (unwrap x) (unwrap y) 方法，这并不是不能容忍的。但我想清楚地了解为什么我不能编写通用的 lift_bin_op_to_wrapped 方法。)

成功编译的完整代码:

%default total

PairedType : (t : Type) -> Type
PairedType t = (t, t)

NatPair : Type
NatPair = PairedType Nat

data WrappedNatPair : Type where
  MkWrappedNatPair : NatPair -> WrappedNatPair

equal_pair : t -> PairedType t
equal_pair x = (x, x)

BinaryOp : Type -> Type
BinaryOp t = t -> t -> t

lift_binary_op_to_pair : BinaryOp t -> BinaryOp (PairedType t)
lift_binary_op_to_pair op (x1, x2) (y1, y2) = (op x1 y1, op x2 y2)

interface Wrapper t where
  WrappedType : Type
  wrap : WrappedType -> t
  unwrap : t -> WrappedType

Wrapper WrappedNatPair where
  WrappedType = NatPair
  wrap x = MkWrappedNatPair x
  unwrap (MkWrappedNatPair x) = x

lift_natpair_bin_op_to_wrapped : BinaryOp NatPair -> BinaryOp WrappedNatPair
lift_natpair_bin_op_to_wrapped op x y = wrap $ op (unwrap x) (unwrap y)

Num WrappedNatPair where
  (+) = lift_natpair_bin_op_to_wrapped (lift_binary_op_to_pair (+))
  (*) = lift_natpair_bin_op_to_wrapped (lift_binary_op_to_pair (*))
  fromInteger x = wrap $ equal_pair (fromInteger x)

WrappedNatPair_example : the WrappedNatPair 8 = (the WrappedNatPair 2) + (the WrappedNatPair 6)
WrappedNatPair_example = Refl

(平台:运行 Idris 1.1.1-git:83b1bed 的 Ubuntu 16.04。)

Answer 1

I think the problem is that t doesn't appear anywhere in the type signature for the Wrapper interface WrapperType method, so WrapperType can't be invoked anywhere other than inside the interface definition itself.

你就在这里。这就是您收到此错误的原因。您可以通过显式指定哪些类型是包装器来修复此编译错误，如下所示:

lift_bin_op_to_wrapped : Wrapper w => BinaryOp (WrappedType {t=w}) -> BinaryOp w
lift_bin_op_to_wrapped {w} op x y = ?hole

但这可能对您没有帮助，因为 Idris 无法推断出 w 和 WrappedType 之间的对应关系。我很想看到对这个事实的解释。基本上编译器(我正在使用 Idris 1.0)告诉我接下来的事情:

- + Wrap.hole [P]
 `--           w : Type
               x : w
               y : w
      constraint : Wrapper w
              op : BinaryOp WrappedType
     -----------------------------------
      Wrap.hole : w

您的WrappedType 依赖类型接口(interface)方法以某种棘手的方式实现类型的模式匹配。我认为这可能是您遇到问题的原因。如果您熟悉 Haskell，您可能会发现 WrappedType 和 -XTypeFamilies 之间存在一些相似之处。看这个问题: Pattern matching on Type in Idris

尽管你仍然可以实现一般的包装函数。您只需要以不同的方式设计您的界面即可。我正在使用这个问题中描述的技巧:Constraining a function argument in an interface

interface Wraps (from : Type) (to : Type) | to where
  wrap   : from -> to
  unwrap : to   -> from

Wraps NatPair WrappedNatPair where
   wrap = MkWrappedNatPair
   unwrap (MkWrappedNatPair x) = x

lift_bin_op_to_wrapped : Wraps from to  => BinaryOp from -> BinaryOp to
lift_bin_op_to_wrapped op x y = wrap $ op (unwrap x) (unwrap y)

Num WrappedNatPair where
  (+) = lift_bin_op_to_wrapped (lift_binary_op_to_pair {t=Nat} (+))
  (*) = lift_bin_op_to_wrapped (lift_binary_op_to_pair {t=Nat}(*))
  fromInteger = wrap . equal_pair {t=Nat} . fromInteger

这可以完美编译并运行。