このNilケースを省略するにはどうすればいいですか？

Question

私はいくつかの一般的なアルゴリズムを実装しているスケーラをぶち壊しています。私はこの問題

に走ったバブルソートを再作成しようとしたときにここでトップに値を泡内部ループの実装です：

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) 
} 

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

Answer 1

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

あなたは、単に case句で遊ぶことができ、その場合には

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)) 
} 

Answer 2

これは、元のタイプの洗練されたにおおよそ対応します。ここでは、メンバが初期タイプのサブセットであるタイプを記述します。その場合、関数への入力がすべてxの場合、そのxはNilではないことを示します。これには十分な証明が必要です（サブタイプタイプを使用して従属タイプのCoqでこれを実装できます）。この場合、より良いことは、Nilのコンストラクタを持たないリストである新しいタイプを導入することです、コンスのコンストラクタと単一の要素のみです。

編集：Scalaでは、List型のサブタイプを使用してこれを強制することができるため、そのサブタイプを使用して型システムでそれを証明できます。これはまだです。つまり、プログラムが実際に何らかの型に存在しているという証拠には、コンパイラが完全に証明できるものです。

Answer 3

注文：

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つのまたは複数の要素をリストに一致します。最後の節は他の部分と一致します。