Простой случай, когда LiquidHaskell хорошо работает с типом "Data.String", но не с типом "Data.Text"

Эта проблема

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

Вот простой пример того, как спецификации Liquid работают хорошо для типа String, но не для типа Text.

Для типа String это работает хорошо

пример

Я определяю тип Liquid, где мы говорим, что значения кортежа не могут быть одинаковыми:

{-@ type NoRouteToHimself = {v:(_, _) | (fst v) /= (snd v)} @-}

Затем для спецификации типа String она работает хорошо, как показано ниже:

{-@ strOk :: NoRouteToHimself @-}
strOk :: (String, String)
strOk = ("AA", "AB")

Выход LiquidHaskel >> РЕЗУЛЬТАТ: БЕЗОПАСНЫЙ

{-@ strBad :: NoRouteToHimself @-}
strBad :: (String, String)
strBad = ("AA", "AA")

Выход LiquidHaskel >> РЕЗУЛЬТАТ: НЕБЕЗОПАСНЫЙ

Пока все хорошо, давайте определим ту же функцию для типа Text.

Для типа текста это идет не так

пример

{-# LANGUAGE OverloadedStrings #-}
import qualified Data.Text as Tx

{-@ foo :: NoRouteToHimself @-}
foo :: (Tx.Text, Tx.Text)
foo = ("AA", "AB")

Ожидаемый результат: РЕЗУЛЬТАТ: БЕЗОПАСНЫЙ

LiquidHaskell Вывод: РЕЗУЛЬТАТ: БЕЗОПАСНЫЙ

 ..Example.hs:102:3-5: Error: Liquid Type Mismatch

 102 |   foo = ("AA", "AB")
         ^^^

   Inferred type
     VV : {v : (Data.Text.Internal.Text, Data.Text.Internal.Text) | x_Tuple22 v == ?a
                                                                    && x_Tuple21 v == ?b
                                                                    && snd v == ?a
                                                                    && fst v == ?b}

   not a subtype of Required type
     VV : {VV : (Data.Text.Internal.Text, Data.Text.Internal.Text) | fst VV /= snd VV}

   In Context
     ?b : Data.Text.Internal.Text

     ?a : Data.Text.Internal.Text

Очевидно, что LiquidHaskell не может оценить значения кортежа для этого случая. Какие-либо предложения?

Источник

2 ответа

Решение

Поработав, я нашел способ сделать это. Я не знаю, как сохранить полиморфизм NoRouteToHimselfНо есть, по крайней мере, способ говорить о равенстве Data.Text объекты.

Метод заключается в том, чтобы ввести меру обозначения. Это Text на самом деле просто причудливый способ представления Stringтак что мы должны в принципе быть в состоянии использовать String рассуждения о Text объекты. Таким образом, мы вводим меру, чтобы получить то, что Text представляет собой:

{-@ measure denot :: Tx.Text -> String @-}

Когда мы строим Text из String, мы должны сказать, что TextОбозначение String мы прошли (это кодирует инъективность, с denot играет роль обратного).

{-@ assume fromStringL :: s:String -> { t:Tx.Text | denot t == s } @-}
fromStringL = Tx.pack

Теперь, когда мы хотим сравнить равенство разных Texts в LH, мы вместо этого сравниваем их обозначения.

{-@ type NoRouteToHimself = v:(_,_) : denot (fst v) /= denot (snd v) @-}

И теперь мы можем получить пример для передачи:

{-@ foo :: NoRouteToHimself @-}
foo :: (Tx.Text, Tx.Text)
foo = (fromStringL "AA", fromStringL "AB")

Чтобы использовать другие функции Data.Text в LH нужно дать денотационные спецификации для этих функций. Это некоторая работа, но я думаю, что это стоит сделать.

Мне любопытно, есть ли способы сделать это лечение более полиморфным и пригодным для повторного использования. Мне также интересно, можем ли мы перегружать понятие равенства ЛХ, чтобы нам не пришлось проходить через denot, Есть чему поучиться.

Источник

Liquid Haskell работает, используя примитивные конструкторы Haskell. String код сахар для

{-@ strOk :: NoRouteToHimself @-}
strOk :: (String, String)
strOk = (,) ('A':'A':[]) ('A':'B':[])

и Liquid Haskell знает, как распутать / отогнать этих конструкторов. Но Data.Text не определяется в терминах конструкторов Haskell, а использует непрозрачную функцию преобразования - -XOverloadedStrings расширение вставляет это:

{-@ foo :: NoRouteToHimself @-}
foo :: (Tx.Text, Tx.Text)
foo = (Tx.pack "AA", Tx.pack "AB")

Здесь Жидкий Хаскелл не знает как Tx.pack работает, дает ли он что-нибудь разрушаемое в своем выводе. Более простой пример, где это также не удается (без -XOverloadedStrings)

{-@ foo :: NoRouteToHimself @-}
foo' :: (String, String)
foo' = (reverse "AA", reverse "AB")

Для того, чтобы это сработало, ЛХ нужно знать, по крайней мере, что Tx.pack а также reverse инъективны Я не знаю достаточно о ЛХ, чтобы сказать, возможно ли достичь этого. Возможно, принуждение к встроенной функции преобразования поможет. Если не считать этого, единственным вариантом будет NF значение и вызвать фактическое == оператор на нем - который будет работать нормально в этом конкретном случае, но был бы невозможен для нетривиальных случаев использования, которые фактически должен делать LH.

Источник
Другие вопросы по тегам