我能否编写一个通用的函数包装函数，用于表示包装另一种类型的类型包装器接口？

Question

下面是一个完整的代码示例（成功编译），它是我问题的一个简化和略有牵强的例子。

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

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

所以，我将其包装在类型“WrappedNatPair”中，并为该类型提供了一个“Num”实现，其中包括“+”和“*”的相应“提升”版本。

然后，我想推广包装器类型的概念，使用我的“Wrapper”接口。

函数“lift_natpair_bin_op_to_wrapped”可以将二元操作从“NatPair”提升到“WrappedNatPair”，并且实现代码完全基于“unwrap”和“wrap”“Wrapper”接口方法。

但是，如果我试图推广到

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接口WrapperType方法的类型签名中，所以WrapperType不能在接口定义之外的任何地方调用。

（解决方法是编写样板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

（平台：Ubuntu 16.04运行Idris 1.1.1-git:83b1bed。）

- Philip Dorrell

Answer 1

我觉得问题在于 Wrapper 接口的 WrapperType 方法的类型签名中没有出现 t，因此除了接口定义本身之外，无法调用 WrapperType。您是正确的。这就是为什么会出现这个错误。您可以通过显式指定 wrapper 的类型来解决这个编译错误，例如：

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依赖类型接口方法以某种棘手的方式实现了类型模式匹配。我认为这可能是你遇到问题的原因。如果你熟悉Haskell，你可能会看到你的WrappedType和-XTypeFamilies之间的一些相似之处。请参考这个问题：Idris中的类型模式匹配 虽然你仍然可以实现通用包装器函数。你只需要以不同的方式设计你的接口。我正在使用这个问题中描述的技巧：约束接口中的函数参数

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

这个程序编译并运行得非常完美。

- Shersh