Как написать простую быструю сортировку на основе списка в Idris? - PullRequest
Новая
       35

Как написать простую быструю сортировку на основе списка в Idris?

0 голосов
/ 08 мая 2018

Я просто пытаюсь сделать минимум, чтобы перевести следующий Haskell на Idris (я не ищу эффективность или доказательства правильности): 

quicksort  []           =  []
quicksort (x:xs)        =  quicksort [y | y <- xs, y<x ]
                        ++ [x]
                        ++ quicksort [y | y <- xs, y>=x]

Вот код Idris, который у меня есть, который практически не отличается от кода на Haskell, за исключением необходимости сообщать Idris, что мы имеем дело с упорядоченными типами: 

quicksort: List (Ord b) -> List (Ord b)
quicksort  []           =  []
quicksort (x::xs)       =  quicksort [y | y <- xs, y<x ]
                        ++ [x]
                        ++ quicksort [y | y <- xs, y>=x]

Тем не менее, я, очевидно, делаю это неправильно. Я вижу, что в вопросе есть ответ на Быстрая сортировка в Идрисе , но форма немного другая - я хотел бы понять, что не так с текущим подходом. Мой код выше выдает ошибку: 

40 | quicksort (x::xs)       =  quicksort [y | y <- xs, y<x ]
   |                            ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
When checking right hand side of quicksort with expected type
        List b

When checking an application of function Prelude.Applicative.guard:
        Can't find implementation for Ord (Ord b)

Ответы [ 2 ]

0 голосов
/ 11 мая 2018

Для пояснения: List (Ord b) - это список реализаций для Ord b, тогда как Ord b => List b - это список b, где b имеет ограничение интерфейса Ord b. Сравните: 

[ord1] Ord Nat where
   compare Z (S n)     = GT
   compare (S n) Z     = LT
   compare Z Z         = EQ
   compare (S x) (S y) = compare @{ord1} x y

imps : List (Ord b) -> List (Ord b)
imps xs = xs

ords : Ord b => List b -> List b
ords xs = xs

С imps [ord1] : List (Ord Nat) и ords [1] : List Nat.

0 голосов
/ 08 мая 2018

Проблема в том, что Prelude.Applicative.guard (функция, которая используется для охранников в списках) не может найти реализацию для Ord класса типов.

Это говорит нам о том, что мы не добавили (или добавили неправильно) ограничение класса типов. Если мы изменим ваш код на этот, он должен работать: 

quicksort: Ord b => List b -> List  b
quicksort  []           =  []
quicksort (x::xs)       =  quicksort [y | y <- xs, y < x ]
                        ++ [x]
                        ++ quicksort [y | y <- xs, y >= x]
...