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

Question

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

NatPair is a pair of Nats, and I want to "lift" the binaryNum operations to NatPair pointwise, using the function lift_binary_op_to_pair.

But I can't implement Num NatPair because NatPair is not a data constructor.

So, I wrap it in a type WrappedNatPair, and I can provide a Num implementation for that type, with corresponding 'lifted' versions of + and *.

Then I want to generalise the idea of a wrapper type, with my Wrapper interface.

The function lift_natpair_bin_op_to_wrapped can lift a binary operation from NatPair to WrappedNatPair, and the implementation code is entirely in terms of the unwrap and wrap Wrapper interface methods.

But, if I try to generalise to

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

then the type signature won't even compile, with 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 error location is the location of ':' in the type signature).

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.

(The workaround is to write boilerplate lift_<wrapped>_bin_op_to_<wrapper> methods with the same implementation code op x y = wrap $ op (unwrap x) (unwrap y) each time, which is not intolerable. But I would like to have a clear understanding of why I can't write the generic lift_bin_op_to_wrapped method.)

The full code which successfully compiles:

%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

(Platform: Ubuntu 16.04 running Idris 1.1.1-git:83b1bed.)

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.

You're right here. This is why you receive this error. You can fix this compilation error by explicitly specifying which types is wrapper like this:

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

But this probably won't help you because Idris somehow cannot deduce correspondence between w and WrappedType. I would love to see explanation of this fact. Basically compiler (I'm using Idris 1.0) says me next things:

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

Your WrappedType dependently typed interface method implements pattern matching on types in some tricky way. I think this might be a reason why you have problems. If you're familiar with Haskell you might see some similarities between your WrappedType and -XTypeFamilies. See this question: Pattern matching on Type in Idris

Though you still can implement general wrapper function. You only need to desing your interface differently. I'm using trick described in this question: 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

This compiles and works perfectly.