An example

• The original function:
  quicksort :: Ord a => [a] -> [a] quicksort [] = [] quicksort (x:xs) = quicksort (filter (<x) xs)++ x: quicksort (filter (>=x) xs)
• The translated function
  quicksort :: Ord a => (xs::[a]) -> Dqs xs -> [a] quicksort [] QsNil = [] quicksort (x:xs) (QsCons x xs p q) = quicksort (filter (<x) xs) p ++ x: quicksort (filter (>=x) xs) q