Liquid Haskell: ошибка «Определение псевдонима циклического типа» из встроенной рекурсивной функции - PullRequest
Новая
       46

Liquid Haskell: ошибка «Определение псевдонима циклического типа» из встроенной рекурсивной функции

0 голосов
/ 21 ноября 2018

Я написал код для выполнения порядковой арифметики в Haskell и сейчас пытаюсь использовать Liquid Haskell для проверки определенных свойств.Однако у меня возникают проблемы с "отражением" рекурсивных функций.Я выделил проблему в функции «меньше чем» ниже: 

-- (Ord a n b) = a^n + b
{-@ data Ordinal [size] = Ord { a :: Ordinal, n :: Nat,  b :: Ordinal }
                        | Zero {} @-}
data Ordinal = Ord Ordinal Integer Ordinal
             | Zero
             deriving (Eq, Show)

{-@ measure size @-}
{-@ size :: Ordinal -> Nat @-}
size :: Ordinal -> Integer
size Zero = 1
size (Ord a n b) = (size a) + 1 + (size b)

{-@ inline ordLT @-}
ordLT :: Ordinal -> Ordinal -> Bool
ordLT _ Zero = False
ordLT Zero _ = True
ordLT (Ord a0 n0 b0) (Ord a1 n1 b1) =
    (ordLT a0 a1) || 
    (a0 == a1 && n0 < n1) || 
    (a0 == a1 && n0 == n1 && ordLT b0 b1)

one = (Ord Zero 1 Zero)     -- 1
w   = (Ord one 1 Zero)      -- omega
main = print w              -- Ord (Ord Zero 1 Zero) 1 Zero

Выполнение liquid ordinals.hs только с вышеприведенным дает следующую ошибку: 

Error: Cyclic type alias definition for `Main.ordLT`
14 |     {-@ inline ordLT @-}
                     ^^^^^
The following alias definitions form a cycle:
* `Main.ordLT`

Так что же такоеправильный способ отразить рекурсивные функции?Я прочитал жидкий урок Haskell , но я не могу понять, что его примеры делают по-другому.

1 Ответ

0 голосов
/ 22 ноября 2018

Немного трудно быть уверенным в том, что вы хотите делать без дополнительного контекста, но inline действительно не работает с рекурсивными функциями: inline позволяет вам использовать функцию типа , расширяя ее ввремя компиляции (до создания условия проверки, отправляемого в решатель), поэтому необходимо иметь возможность заменить каждое вхождение ordLT a b какой-то определенной логической формулой (что невозможно, поскольку это рекурсивно).

Если вам нужно использовать произвольные функции Haskell в логике, вы можете изучить использование Refinement Reflection.Ваш пример компилируется с {-@ reflect ordLT @-} и {-@ LIQUID "--exact-data-cons" @-}.Однако символы функций, созданные с помощью уточненного отражения, не полностью интерпретируются в логике.Мельчайшие подробности обсуждаются в этой статье , а более доступные примеры / объяснения представлены в этих слайдах и в этом посте .Главное, что нужно помнить, это то, что символ ordLT, созданный с помощью отражения, первоначально будет рассматриваться как совершенно не интерпретируемая функция в логике: единственное, что LH знает об этом, это что-то вроде a0 == a1 ==> b0 == b1 ==> ordLT a0 b0 == ordLT a1 b1 (если вы вызываете его на идентичных входах(результаты идентичны).

Чтобы сделать что-то полезное с ordLT в логике, вам нужно будет вызвать ordLT на уровне значений где-то в области видимости, который покажет значениеэтот конкретный вызов, поскольку тип возвращаемого значения ordLT (функция уровня значения) утверждает что-то о выводе ordLT (неинтерпретируемой функции логического уровня) на этих входах.Примеры приведены в слайдах, связанных выше, и в документе.Надеюсь, этого достаточно, чтобы вы начали!

...