Описание тега liquid-haskell

Описание тега Вопросы с тегом
По вопросам, относящимся к статическому верификатору LiquidHaskell.
0 ответов

Как установить жидкий haskell в Ubuntu 18.04?

Я изо всех сил пытаюсь установить жидкий Haskell в Ubuntu 18.04. Я пробовал несколько команд для установки зависимостей и теперь получаю сообщение об ошибке при окончательной компиляции жидкого Haskell. Я использую следующую команду для установки: К…
18 ноя '18 в 13:42
1 ответ

Как указать функцию, работающую с непустой структурой данных, с помощью LiquidHaskell?

Я пытаюсь выполнить первое упражнение в тематическом исследовании LiquidHaskell о Lazy Queues module Main where main :: IO () main = putStrLn "hello" {-@ type Nat = {v:Int | 0 <= v} @-} {-@ die :: {v:String | false} -> a @-} die x = error x {-…
22 фев '16 в 01:19
1 ответ

"Типовые термины" во время выполнения в LiquidHaskell vs. Idris

В последнее время я играл с LiquidHaskell и Idris, и у меня возник довольно специфический вопрос, который я нигде не мог найти однозначного ответа. Идрис - это типизированный язык, который по большей части хорош. Однако я читал, что некоторые термин…
14 дек '18 в 23:14
2 ответа

Возврат подмножества типов в Haskell

Я пытаюсь ограничить тип возвращаемого значения функции для подмножества (добрых) конструкторов. Я могу использовать классы типов для ограничения типов ввода, но когда я пытаюсь использовать ту же технику для типов возврата, как показано ниже, я пол…
21 июл '18 в 23:50
1 ответ

Есть ли в Liquid Haskell включенная прелюдия?

Есть ли аннотированный вариант или Haskell Prelude для легкой миграции существующих программ, которые вызывают такие функции, как head или же length?
31 янв '16 в 18:26
1 ответ

Могу ли я определить параметрический тип данных, где параметры не равны между собой в Haskell?

Проблема: Давайте представим, что у нас есть Пассажир с начальной и конечной точками, представленными: data Passenger a = Passenger { start :: a , end :: a } Вопрос: Как я могу применить ограничения класса к Пассажиру, где начальная точка не должна …
28 дек '18 в 16:51
0 ответов

Жидкий haskell создает новую бистринг с PS

Я делаю некоторые привязки к C из Haskell и пытаюсь сделать его более безопасным с помощью LiquidHaskell. У меня возникли проблемы с указанием длины строки байтов в аннотации типа LH. У меня есть расширенный тип ByteString в LiquidHaskell, который в…
30 ноя '18 в 17:58
1 ответ

Использование Liquid Haskell для проверки на наличие токенов

Я делаю некоторые эксперименты с использованием Liquid-Haskell, чтобы увидеть, какие аккуратные вещи я могу сделать с ним, и я ударился об стенку. Основная идея заключается в том, что у меня есть некоторые функции, для которых требуется токен доступ…
14 авг '16 в 01:32
1 ответ

LiquidHaskell: пытается использовать ключевое слово предположить, но тип данных не числовой

Я пытаюсь написать некоторые спецификации для Data.Ratio модуль. Пока что у меня есть: module spec Data.Ratio where import GHC.Real Data.Ratio.denominator :: GHC.Real.Integral a => r : GHC.Real.Ratio a -> {x:a | x > 0} Код, который я провер…
25 июл '17 в 12:50
0 ответов

Liquid haskell говорит, что сервер безопасен, когда это не так

У меня есть сервер в Haskell, который отвечает на входные данные Json. Проблема в том, что в некоторых случаях происходит сбой сервера из-за частичной функции, но Liquid Haskell утверждает, что это безопасно. Вот минимальный рабочий пример: {-# LANG…
30 мар '18 в 12:04
1 ответ

Могу ли я использовать Liquid Haskell для кода, который требует GHC 8?

У меня есть проект, который собран со стеком и требует GHC 8. Можно ли использовать Liquid Haskell с моим проектом, учитывая, что он требует GHC 8? Если да, то как мне установить и запустить Liquid Haskell? Спасибо!
27 дек '16 в 22:24
1 ответ

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

Я написал некоторый код для выполнения порядковой арифметики в Haskell и теперь пытаюсь использовать Liquid Haskell для проверки определенных свойств. Однако у меня возникают проблемы с "отражением" рекурсивных функций. Я выделил проблему в функции …
21 ноя '18 в 19:06
2 ответа

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

Эта проблема Я был очень взволнован, играя с LiquidHaskell, однако я не знаю, в какой степени мне нужно изменить свой исходный код на Haskell, чтобы он соответствовал требованиям LiquidHaskell. Вот простой пример того, как спецификации Liquid работа…
04 фев '19 в 18:32
1 ответ

LiquidHaskell: нарушение закона Деморгана

У меня проблемы с доказательством следующего закона с LiquidHaskell: Он известен как (один из) закон Деморгана, и просто утверждает, что отрицание orДва значения должны быть такими же, как andотрицание каждого. Это было доказано в течение долгого вр…
23 апр '16 в 16:38
1 ответ

Кто-нибудь смог интегрировать liquidhaskell с nixos?

Я пытаюсь использовать liquidhaskell на NixOS. Я могу установить пакет (liquidhaskell-0.8.2.3), но не для интеграции с Cabal, потому что для этого требуется Cabal 1.18-1.25, но у меня есть Cabal 2.0.1.0 . Я установил пакет liquidhaskell как часть ус…
06 мар '18 в 12:03
1 ответ

Liquid Haskell: ошибка с проверочными комбинаторами и типы, уточненные предикатами

В качестве минимального примера проблемы, которую я имею, вот определение натуральных чисел, функции удвоения и типа, уточненного предикатом четности: data Nat' = Z | S Nat' deriving Show {-@ reflect double' @-} double' :: Nat' -> Nat' double' Z …
28 ноя '18 в 20:47
1 ответ

Что такое мера?

Я читаю это, где я нахожу это: Меры - чтобы позволить функциям Haskell появляться в типах уточнения, нам необходимо поднять их до уровня типа уточнения. И есть другие документы, утверждающие, что необходимы меры для использования такой функции в кон…
30 май '19 в 10:55
1 ответ

Каков правильный контракт функции "карта" в Liquid Haskell?

Я пытаюсь выполнить упражнение из руководства LiquidHaskell. Итак, я написал это: data List a = Nil | Cons a (List a) deriving (Show) infixr 5 `Cons` {-@ len :: List a -> Nat @-} len :: List a -> Int len Nil = 0 len (x `Cons` xs) = 1 + len xs …
27 май '19 в 12:38
1 ответ

Верны ли эти примеры или учебник содержит ошибку?

Я читаю этот учебник, и я не уверен, что я правильно понимаю текст (или что он является правильным в целом). Вот пример: Следующие предикаты действительны, потому что они кодируют modus ponens: если вы знаете, что a подразумевает b, и знаете, что a …
29 май '19 в 13:24
2 ответа

Можно ли использовать однострочные контракты в Liquid Haskell?

Liquid Haskell использует комментарии как {-@ ... @-} для контрактов блок. Можно ли (с параметром командной строки, конфигурационным файлом) указать, использовать ли однострочный стиль комментариев, например -- ... для контрактов?
23 май '19 в 13:53