¿Cómo puedo omitir este caso Nil

Question

Estoy haciendo tonterías con scala implementando algunos algoritmos comunes. Al intentar volver a crear una especie de burbuja me encontré con este problema

Aquí es una implementación de un bucle interno que burbujea el valor de la parte superior:

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

Mi problema es con el caso Nil => Nil. Entiendo que necesito esto porque podría aplicar Nil a esta función. ¿Hay alguna forma de garantizar que Nil no se pueda proporcionar como argumento de manera que satisfaga al compilador para que pueda eliminar este caso?

Answer 1

La lista tiene dos subtipos, Nil y ::, entonces :: representa una lista que tiene al menos un elemento.

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

Esto correspondería más o menos a un refinamiento del tipo original, donde escribiría un tipo cuyos miembros eran un subconjunto del tipo inicial. A continuación, mostraría que, para cada entrada x a su función, esa x no era Nil. Como esto requiere una buena cantidad de pruebas (puede implementar esto en Coq con tipos dependientes usando un tipo de subconjunto ), lo mejor que puede hacer en esta situación podría ser introducir un nuevo tipo, que era una lista que no tiene Nil constructor , solo un constructor de contras y un solo elemento.

EDITAR: Como Scala le permite usar el subtipado sobre el tipo de lista para imponer esto, puede probarlo en el sistema de tipos de manera decidible utilizando ese subtipo. Esto es todavía una prueba, en el sentido de que cualquier verificación de tipo corresponde a una prueba de que el programa efectivamente habita de algún tipo, es algo que el compilador puede probar completamente.

Answer 3

En ese caso, puede simplemente jugar con las cláusulas case orden:

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 
} 

Las primeras dos cláusulas sólo igualará listas con uno o más elementos. La última cláusula coincidirá en otro lugar.