我可以为Wrapper接口编写一个通用的函数包装函数来表示包装其他类型的类型吗？

2023年7月23日 283次阅读

下面的完整代码示例(成功编译)是我的问题的简化和轻微设计的示例.

NatPair是一对Nats,我想使用函数lift_binary_op_to_pair将binaryNum操作“提升”到NatPair.

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

因此,我将它包装在WrappedNatPair类型中,并且我可以为该类型提供Num实现,具有相应的’提升’版本和*.

然后我想用我的Wrapper接口来概括包装类型的概念.

函数lift_natpair_bin_op_to_wrapped可以解除NatPair的二进制操作
到WrappedNatPair,实现代码完全是在unwrap和
包装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不能在除了inside之外的任何地方调用
接口定义本身.

(解决方法是每次使用相同的实现代码op xy = wrap $op(unwrap x)(展开y)编写样板lift_< wrapped> _bin_op_to_< wrapper>方法,这是不可忍受的.但我想要一个清楚地理解为什么我不能写出通用的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.)

最佳答案

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依赖类型接口方法以某种棘手的方式在类型上实现模式匹配.我想这可能是你遇到问题的原因.如果您熟悉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

这编译并完美地工作.

点赞