Простой случай, когда LiquidHaskell хорошо работает с типом «Data.String», но не с типом «Data.Text» - PullRequest
Новая
       20

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

0 голосов
/ 04 февраля 2019

Проблема

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

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

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

Пример

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

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

Тогда для String *Спецификация типа 1021 * работает хорошо, как показано ниже: 

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

Выход LiquidHaskel >> РЕЗУЛЬТАТ: SAFE 

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

Выход LiquidHaskel >> RESULT: UNSAFE

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

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

Пример 

{-# 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 ]

0 голосов
/ 05 февраля 2019

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

Метод состоит в том, чтобы ввести мера обозначения .То есть Text - это на самом деле просто причудливый способ , представляющий a 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

Теперь, когда мы хотим сравнить равенство различных Text s в 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.Есть чему поучиться.

0 голосов
/ 05 февраля 2019

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

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

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

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

...