2017-10-02 14 views
3

Idrisでは、述語に基づいて要素を削除したい場合、filter,dropWhiletakeWhileがあります。ただし、これらの関数はすべて、従属ペア(n : Nat ** Vect n elem)を返します。Idris判定結果のベクトル長

Vectタイプとして返​​される関数はありますか?私は考えることができるものについては

  1. 変換後の長さのベクトルを示すタイプを実装Vect

  2. に依存ペアに変換Hereのように、(私はどのように分からないと思いました)上記のアイデアについては、There

、(すべての再変換1のために非常に面倒なようですsult)または2(結果ベクトルの長さを示す型をそれぞれ設計する)。

このような動作を実現する方法はありますか?

dropElem : String -> Vect n String -> Vect ?resultLen String

答えて

1

たぶん、これはあなたが探しているものでしょうか?

dropElem: (s: String) -> (v: Vect n String) -> Vect (count ((/=) s) v) String 
dropElem s = filter ((/=) s) 

あなたも、既存のfilter実装再利用することができます:

import Data.Vect 

count: (ty -> Bool) -> Vect n ty -> Nat 
count f [] = 0 
count f (x::xs) with (f x) 
    | False = count f xs 
    | True = 1 + count f xs 

%hint 
countLemma: {v: Vect n ty} -> count f v `LTE` n 
countLemma {v=[]} = LTEZero 
countLemma {v=x::xs} {f} with (f x) 
    | False = lteSuccRight countLemma 
    | True = LTESucc countLemma 

filter: (f: ty -> Bool) -> (v: Vect n ty) -> Vect (count f v) ty 
filter f [] = [] 
filter f (x::xs) with (f x) 
    | False = filter f xs 
    | True = x::filter f xs 

次にあなたが詐欺これを行う

count: (ty -> Bool) -> Vect n ty -> Nat 
count f v = fst $ filter f v 

filter: (f: ty -> Bool) -> (v: Vect n ty) -> Vect (count f v) ty 
filter f v = snd $ filter f v 
+0

を私は 'countLemma'が必要とされていないことに気づきました。他の場所で役に立つかもしれないので、私はそこに残します。 https://stackoverflow.com/questions/46528291/can-idris-infer-indices-in-types-of-top-level-constantsが積極的に回答されると、結果の種類を書き留めるのが簡単になります。 – Gregg54654

+0

結果は、結果の 'vect'長さをあらかじめ計算することです。したがって、それは型チェッカーを渡しますか? – gostriderful

+0

はい、それはあなたの例の '?resultLen'の略です:結果のベクトルの長さとそれを知る必要があります。結果のベクトルの長さが追跡するのが複雑になる場合は、ユースケースに応じて複数のオプションがあります。長さを追跡しない 'List'や、知っておく必要のあるプロパティだけを追跡するカスタムデータ型を使うことができます。たとえば、長さの上限です。 – Gregg54654

関連する問題