Can I write a generic function wrapper function for a Wrapper interface representing a type that wraps some other type?

Question

The full code example below (which compiles successfully) is a simplified and slightly far-fetched example of my problem.

NatPairrepresents a pair of Nats, and I want to “raise” binary operations Numto NatPairpointwise using a function lift_binary_op_to_pair.

But I can not implement Num NatPair, because it is NatPairnot a data constructor.

So, I transfer it to a type WrappedNatPair, and I can provide an implementation Numfor this type with the corresponding "canceled" versions +and *.

Then I want to generalize the idea of ​​a shell type with my interface Wrapper.

A function lift_natpair_bin_op_to_wrappedcan raise a binary operation from NatPair to WrappedNatPair, and the implementation code is entirely in terms unwrapand wrap Wrappermethods of the interface.

But if I try to generalize to

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

then the type signature will not even compile with an error:

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

(where the location of the error is the location ":" in the type signature).

I think the problem is that it tdoes not appear anywhere in the type for the interface Wrapper WrapperType, so WrapperTypeit cannot be called anywhere except inside the interface definition itself.

(The workaround is to write boilerplate methods lift_<wrapped>_bin_op_to_<wrapper>with the same implementation code op x y = wrap $ op (unwrap x) (unwrap y)every time that is unbearable. But I would like to have a clear idea of ​​why I cannot write a generic one lift_bin_op_to_wrapped.)

Full code that compiles successfully:

%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.)

Answer 1

, , t WrapperType- Wrapper, WrapperType , .

. . , , :

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

, , , - 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. . :

. -. , :

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

.