2017-10-25 6 views
1

私は、バイナリと単項関数からツリーとして構築された、n-ary関数の従属型を定義しようとしています;これは(Vect n a) -> aの型と同型です) Idrisを学ぶ練習として。mと(マイナスm 0)の間のタイプの不一致

n項関数に引数を適用する関数を定義しようとしている((N-1)進機能を生成する)一方で、私は非常に疑わしいエラーを得た:

Type mismatch between 
      ArityFn m a (Type of ng) 
    and 
      ArityFn (minus m 0) a (Expected type) 

    Specifically: 
      Type mismatch between 
        m 
      and 
        minus m 0 

は、ここでのコードです質問のため

data ArityFn : Nat -> (ty: Type) -> Type where 
    Val  : (x : ty) -> ArityFn 0 ty 
    UnaryFn : (ty -> ty) -> ArityFn 1 ty 
    BinaryFn : (ty -> ty -> ty) -> ArityFn 2 ty 
    NAryFn : (ty -> ty -> ty) -> (ArityFn n ty) -> (ArityFn m ty) -> ArityFn (n + m) ty 

%name ArityFn nf, ng, nh 

applyArityFn : a -> (ArityFn n a) -> (LTE 1 n) -> ArityFn (n - 1) a 
... (some definitions elided) 
applyArityFn x (NAryFn h (UnaryFn f) ng) _ = mkNAryFn h (Val (f x))  ng 

これは型チェッカーのバグですか?

:def minus戻ります(他のもののうち、いくつかのクリーンアップを法):

Original definiton: 
minus 0 right = 0 
minus left 0 = left 
minus (S left) (S right) = minus left right 

をあなたはminus left 0 = leftがないことを見ることができます疑いで、捕まってしまった関数の定義を探し

+2

関連:[1](https://stackoverflow.com/q/42534191/2747511)、[2](https://stackoverflow.com/questions/45744130/plus-vs-s-in- a関数型)。 –

答えて

3

前にパターンminus 0 right = 0があるので、定義的に保持する。もちろん、両方の式が一致すると同じ結果を返しますが、idrisはそのことを知らないのです。 mで何とかパターンマッチのいずれか

  • minusはその最初の引数が証拠によって
  • や書き換えを露出されるのヘッドコンストラクタということになりまし減らすために得る:

    あなたはあなたができる望む結果を得るために、 minus m 0 = m

+2

最後の提案では、minusZeroRight :(左:Nat) - >左(fromInteger 0)=左 'のような補題があります。 –

+0

今私は非常に混乱しています。 「マイナス左0 =左」は定義上保持されませんか?それは文字通り定義的です! – colinro

+2

しかし、マイナス0右= 0で影を付けています:パターンが宣言された順序は重要です!これは、第1引数にケースツリーを分割することになります。これは、「マイナス左0 =左」に対応するが、定義的に保持する方程式は、「マイナス0 0 = 0」とマイナス(Sの左)0 = S '。 Agdaには、これが混乱しているため正確に把握できない式を強調表示する「正確な分割」警告があります。 – gallais

関連する問題