Stack Overflow
Stack Overflow

Questions tagged [liquid-haskell]

For questions pertaining to the LiquidHaskell static verifier.

LiquidHaskell is a static verifier which works with the Haskell language.

LiquidHaskell itself is based upon Liquid Types, and aims to help write memory-safe, but also provably correct programs by allowing users to annotate types with logical constraints which can later be solved using SMT solvers.

37 questions
10
votes
1 answer

What is a measure?

I am reading this where I find this: Measures -- In order to allow Haskell functions to appear in refinement types, we need to lift them to the refinement type level. And there are other documents asserting that measures are needed to use such…
RandomB
  • 3,367
  • 19
  • 30
8
votes
1 answer

What is the correct contract of the function "map" in Liquid Haskell?

I am trying to solve some exercise from LiquidHaskell tutorial. So, I wrote this: data List a = Nil | Cons a (List a) deriving (Show) infixr 5 `Cons` {-@ len :: List…
RandomB
  • 3,367
  • 19
  • 30
8
votes
0 answers

Liquid haskell says server is safe when it isn't

I have a server in Haskell that responds to Json inputs. The problem is that there are cases where the server will crash because of a partial function, but Liquid Haskell says it is safe. Here's a minimal working example: {-# LANGUAGE…
8n8
  • 1,233
  • 1
  • 8
  • 21
7
votes
1 answer

Simple congruence proof error with Liquid Haskell - Liquid Type Mismatch

I'm following the official tutorial on Liquid Haskell, and stumbled upon what seems to be a "bug" in it. The following code is present in the tutorial, and Liquid Haskell was supposed to check that it is safe. {-@ type TRUE = {v:Bool | v }…
Thales MG
  • 761
  • 5
  • 15
7
votes
1 answer

Runtime "type terms" in LiquidHaskell vs. Idris

I have been playing around with LiquidHaskell and Idris lately and i got a pretty specific question, that i could not find a definitive answer anywhere. Idris is a dependently typed language which is great for the most part. However i read that some…
Lazarus535
  • 1,158
  • 1
  • 8
  • 23
6
votes
0 answers

Syntax for using datatype indexed by Nat

The following code tries to refine Clash's Unsigned type family at index 4 into Digit: import Clash.Prelude {-@ type Digit = {v : Unsigned 4 | v <= 9 } @-} type Digit = Unsigned 4 {-@ foo :: Digit -> Digit @-} foo = id @Digit This leads to the…
Cactus
  • 27,075
  • 9
  • 69
  • 149
6
votes
2 answers

A simple case where LiquidHaskell works well on the type "Data.String" but not on the type "Data.Text"

The problem I've been very excited playing with LiquidHaskell, however, I don't know to what extent I need to modify my original Haskell code to meet LiquidHaskell's requirements. Here is a simple example of how Liquid's specifications work well for…
racherb
  • 335
  • 1
  • 10
6
votes
1 answer

Has anyone been able to integrate liquidhaskell with nixos?

I'm trying to use liquidhaskell on NixOS. I can install the package (liquidhaskell-0.8.2.3), though not the cabal integration, because it requires cabal 1.18-1.25, but I have cabal 2.0.1.0 . I have installed the liquidhaskell package as part of a…
user3416536
  • 1,429
  • 9
  • 20
5
votes
1 answer

Expressive power of Liquid Haskell

Following up from my recent question, I have been pondering over the following: We can create some new amazing types in LH, particularly, express some non-trivial subsets of Integers. For example: {-@ type Nat = {v:Int | v>=0 } @-} {-@ type grtN N =…
kishlaya
  • 453
  • 2
  • 14
5
votes
1 answer

Defining measures in Liquid Haskell

Here's a simple function to calculate average of the numbers in a given list. {-@ type NonZero = {v:Int | v/=0 } @-} {-@ divide :: Int -> NonZero -> Int @-} divide :: Int -> Int -> Int divide n d = div n d {-@ measure nonEmpty :: [a] -> Bool…
kishlaya
  • 453
  • 2
  • 14
5
votes
1 answer

LiquidHaskell: failing DeMorgan's law

I am having troubles proving the following law with LiquidHaskell: It is known as (one of) DeMorgan's law, and simply states that the negation of oring two values must be the same as anding the negation of each. It's been proven for a long time,…
Nicolas Mattia
  • 1,269
  • 11
  • 20
5
votes
1 answer

Is there Liquid Haskell enabled Prelude?

Is there a annotated variant or Haskell Prelude available for easy migration of existing programs that call functions like head or length?
sevo
  • 4,559
  • 1
  • 15
  • 31
4
votes
1 answer

Liquid Haskell: "Cyclic type alias definition" error from an inlined recursive function

I wrote some code to do ordinal arithmetic in Haskell and am now trying to use Liquid Haskell to verify certain properties. However, I'm having trouble "reflecting" recursive functions. I've isolated a problem in the "less than" function below: --…
Alex Varga
  • 1,752
  • 2
  • 14
  • 17
4
votes
1 answer

LiquidHaskell: Trying to use assume keyword, but data type is not numeric

I'm trying to write some specifications for the Data.Ratio module. So far I have: module spec Data.Ratio where import GHC.Real Data.Ratio.denominator :: GHC.Real.Integral a => r : GHC.Real.Ratio a -> {x:a | x > 0} The code I'm verifying is: {-@…
limick
  • 55
  • 3
3
votes
0 answers

Need help installing LiquidHaskell on Ubuntu

for my bachelor thesis I want to write about and do a few experiments with LiquidHaskell. I already installed Haskell/GHC and CVC4 as SMT Solver. Now I am trying to install the liquid-package on my Ubuntu-Laptop but run into problems: If I try the…
Noodlez
  • 31
  • 1
1
2 3