他の型をラップする型を表すWrapperインタフェース用の汎用ラップ関数を記述できますか？

Question

下記の完全なコード例（正常にコンパイルされたもの）は、私の問題の単純化されたやや工夫された例です。

NatPairはNat秒のペアである、と私は機能lift_binary_op_to_pairを使用して「リフト」NatPair点ごとにバイナリNum操作、したいです。

を実装することはできません。NatPairはデータコンストラクタではないためです。

だから、私はタイプWrappedNatPairでそれをラップし、私は+と*の対応「持ち上げる」バージョンでは、そのタイプのNum実装を提供することができます。

次に、Wrapperインターフェイスを使用して、ラッパータイプのアイデアを一般化したいと考えています。

lift_natpair_bin_op_to_wrapped

機能はWrappedNatPairにNatPair からバイナリ操作を持ち上げることができ、実装コードはunwrapと wrapWrapperインタフェースメソッドの点で完全です。

しかし、私はエラーで、その後、型シグネチャもコンパイルされません

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がそうWrapperTypeが インタフェース定義自体の内部以外の場所に起動することはできませんWrapperインタフェースWrapperType方法、 のためにどこでも 型シグネチャで表示されないということだと思います。

（回避策は耐え難いされていない、同じ実装コードop x y = wrap $ op (unwrap x) (unwrap 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実行イドリス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.

あなたはここにいます。このため、このエラーが発生します。

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依存型指定されたインターフェイスメソッドは、いくつかのトリッキーな方法で型にパターンマッチングを実装します。私はこれがあなたに問題がある理由かもしれないと思う。ハスケルに精通している場合は、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 

：私はこの質問で説明したトリックを使用しています。