5

いくつかの一般的なアルゴリズムを実装するscalaをいじっています。バブルソートを再作成しようとしているときに、この問題に遭遇しました

値を一番上にバブルする内部ループの実装を次に示します。

def pass(xs:List[Int]):List[Int] = xs match { 
  case Nil => Nil 
  case x::Nil => x::Nil 
  case l::r::xs if(l>r) => r::pass(l::xs)
  case l::r::xs => l::pass(r::xs)
}

私の問題は caseNil => Nilです。私はNilこの機能に適用できるので、これが必要であることを理解しています。Nilこのケースを排除できるように、コンパイラを満足させる方法で引数として提供できないようにする方法はありますか?

4

3 に答える 3

4

List には Nil と :: の 2 つのサブタイプがあるため、:: は少なくとも 1 つの要素を持つリストを表します。

def pass(xs: ::[Int]):List[Int] = xs match { 
  case x::Nil => x::Nil 
  case l::r::xs if(l>r) => r::pass(new ::(l,xs))
  case l::r::xs => l::pass(new ::(r, xs))
}
于 2012-09-30T16:09:19.837 に答える
2

これは、元の型の改良にほぼ対応し、メンバーが初期型のサブセットである型を記述します。x次に、関数へのすべての入力について、それxが非 であったことを示しますNil。これにはかなりの量の証明が必要なので（サブセットNil型を使用して依存型を使用してCoqでこれを実装できます）、この状況で行う方がよいのは、コンストラクターがなく、コンストラクターのみを持つリストである新しい型を導入することです。短所と単一要素のコンストラクタ。

編集：Scalaではリスト型に対してサブタイピングを使用してこれを強制できるため、そのサブタイプを使用して型システムでそれを明確に証明できます。これは、プログラムが実際に何らかの型に存在するという証明に対応するという意味で、まだ証明です。これは、コンパイラが完全に証明できるものにすぎません。

于 2012-09-30T15:55:30.993 に答える
2

その場合、case句の順序を単純に試すことができます。

def pass(xs:List[Int]):List[Int] = xs match { 
  case l::r::xs if(l>r) => r::pass(l::xs)
  case l::r::xs => l::pass(r::xs)
  case xs => xs
}

最初の 2 つの句は、1 つ以上の要素を持つリストのみに一致します。最後の句は他の場所と一致します。

于 2012-09-30T16:34:48.357 に答える