LiquidHaskell

https://ucsd-progsys.github.io/liquidhaskell
Admin
LiquidHaskell is a type checker that refines Haskell's types with logical predicates to enforce...
Tokens:227,817
Snippets:1,862
Trust Score:9.7
Update:6 months ago
Show doc for...
Tokens:
Raw
### Example: Accepted SList Construction

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2015-01-30-okasakis-lazy-queue.lhs

Demonstrates the construction of a valid SList that meets the size invariant. This example is accepted by LiquidHaskell.

```Haskell
160: okList  = SL 1 ["cat"]    -- accepted

```

--------------------------------

### Example Usage of charFrequency

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2013-01-31-safely-catching-a-list-by-its-tail.lhs

Provides a concrete example of how to use the charFrequency function with a list of sample words.

```Haskell
f0 = charFrequency [ "the", "quick" , "brown"
                   , "fox", "jumped", "over"
                   , "the", "lazy"  , "cow"   ]
```

--------------------------------

### Example Matrix Definition

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2013-02-16-kmeans-clustering-I.lhs

Provides a concrete example of a 4x2 matrix and its transposed 2x4 counterpart.

```haskell
m1  :: Matrix Int 4 2
m1  =  [ [1, 2]
       , [3, 4]
       , [5, 6]
       , [7, 8] ]
```

```haskell
m2 :: Matrix Int 2 4
m2  =  [ [1, 3, 5, 7]
       , [2, 4, 6, 8] ]
```

--------------------------------

### Haskell Example: Zeroing 4 Bytes

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_11_Case_Study_Pointers.html

An example function that allocates a 4-byte buffer, fills it with zeros using poke and plusPtr, and returns the ForeignPtr.

```haskell
zero4 = do fp <- mallocForeignPtrBytes 4
withForeignPtr fp $ \p -> do
poke (p `plusPtr` 0) zero
poke (p `plusPtr` 1) zero
poke (p `plusPtr` 2) zero
poke (p `plusPtr` 3) zero
return fp
where
zero = 0 :: Word8
```

--------------------------------

### LiquidHaskell Environment Example

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_02_Logic.html

Illustrates an environment mapping variables to their Haskell types.

```haskell
x :: Int
y :: Int
z :: Int
```

--------------------------------

### Initialize LiquidHaskell Module

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2013-01-01-refinement-types-101.lhs

Basic module setup including the required LiquidHaskell prelude import.

```haskell
42: module Intro where
43: 
44: import Language.Haskell.Liquid.Prelude  (liquidAssert)
```

--------------------------------

### Demonstrate Subtyping with Zero

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_03_Basic.html

Examples showing how a single value can satisfy multiple refinement types.

```haskell
{-@ zero' :: Nat @-}
zero' = zero
```

```haskell
{-@ zero'' :: Even @-}
zero'' = zero
```

```haskell
{-@ zero''' :: Lt100 @-}
zero''' = zero
```

--------------------------------

### Explode Function Example

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2013-12-02-getting-to-the-bottom.lhs

An example demonstrating potential issues with bottom values in expressions.

```haskell
70: explode = let z = 0
71:           in  (\x -> 2013 `divide` z) (foo z)
```

--------------------------------

### Example AVL Tree Structure (ghci)

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_12_Case_Study_AVL.html

An example of an AVL tree structure as represented in GHCi, showing keys, left/right children, and the stored height (ah).

```Haskell
ghci> let t0 = Node { key = 'a'
                    , l   = Leaf
                    , r   = Node {key = 'd'
                                 , l  = Leaf
                                 , r  = Leaf
                                 , ah = 1 }
                    , ah = 2}
```

--------------------------------

### LiquidHaskell Assignment Example

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_02_Logic.html

Demonstrates an assignment of values to variables under a given environment.

```haskell
x := 1
y := 2
z := 3
```

--------------------------------

### Importing Data.Set for LiquidHaskell

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2013-03-26-talking-about-sets.lhs

Initial module setup for working with sets in LiquidHaskell.

```haskell
27: module TalkingAboutSets where
28: 
29: import Data.Set hiding (filter, split)
30: import Prelude  hiding (reverse, filter)
31: 
```

--------------------------------

### Example Usage of Dependent Tuples

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2013-07-29-putting-things-in-order.lhs

An example demonstrating the instantiation of a dependent tuple type with a specific refinement for a list of integer pairs.

```Haskell
240: {-@ plusOnes :: [(Int, Int)<{\x1 x2 -> x2 = x1 + 1}>] @-} 
```

--------------------------------

### Example Binary Search Tree Value

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_05_Datatypes.html

An example of a valid Binary Search Tree with integer values, demonstrating the structure and ordering.

```haskell
okBST :: BST Int
okBST = Node 6
(
Node 2
(
Node 1 Leaf Leaf
)
(
Node 4 Leaf Leaf
)
)
(
Node 9
(
Node 7 Leaf Leaf
)
Leaf
)
```

--------------------------------

### Initialize Monomorphic Association Lists

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2013-07-29-putting-things-in-order.lhs

Example instances of monomorphic association lists with specific key-value pairs.

```haskell
126: digits    :: Assoc String
127: (PuttingThingsInOrder.Assoc [(GHC.Types.Char)])digits    = forall <p :: (GHC.Types.Int)-> Bool>.
[({VV : (GHC.Types.Int)<p> | true}, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)})]
-> (PuttingThingsInOrder.Assoc <p> {VV : [(GHC.Types.Char)] | ((len VV) >= 0)})KV [ ({VV : (GHC.Types.Int) | (VV == 1) && (VV > 0)}, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)})<\_ VV -> ((len VV) >= 0)>({VV : (GHC.Types.Int) | (VV == (1  :  int))}1, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"one")
128:                , ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 9)}, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)})<\_ VV -> ((len VV) >= 0)>({VV : (GHC.Types.Int) | (VV == (2  :  int))}2, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"two")
129:                , ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 9)}, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)})<\_ VV -> ((len VV) >= 0)>({VV : (GHC.Types.Int) | (VV == (3  :  int))}3, {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"three") ]
130: 
131: sparseVec :: Assoc Double
132: (PuttingThingsInOrder.Assoc (GHC.Types.Double))sparseVec = forall <p :: (GHC.Types.Int)-> Bool>.
[({VV : (GHC.Types.Int)<p> | true}, (GHC.Types.Double))]
-> (PuttingThingsInOrder.Assoc <p> (GHC.Types.Double))KV [ ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 1000)}, (GHC.Types.Double))({VV : (GHC.Types.Int) | (VV == (12  :  int))}12 ,  (GHC.Types.Double)34.1 )
133:                , ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 1000)}, (GHC.Types.Double))({VV : (GHC.Types.Int) | (VV == (92  :  int))}92 , (GHC.Types.Double)902.83)
134:                , ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 1000)}, (GHC.Types.Double))({VV : (GHC.Types.Int) | (VV == (451  :  int))}451,   (GHC.Types.Double)2.95)
135:                , ({VV : (GHC.Types.Int) | (VV > 0) && (0 <= VV) && (VV <= 1000)}, (GHC.Types.Double))({VV : (GHC.Types.Int) | (VV == (877  :  int))}877,   (GHC.Types.Double)3.1 )]
```

--------------------------------

### Example Queues for Type Checking

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_09_Case_Study_Lazy_Queues.html

Defines example queues with specific sizes for testing LiquidHaskell's type checking capabilities, particularly for the `remove` function.

```Haskell
okRemove = remove example2Q -- accept
```

```Haskell
badRemove = remove example0Q -- reject
```

```Haskell
{-@ example2Q :: QueueN _ 2 @-} 
example2Q = Q (1 `cons` (2 `cons` nil)) nil
```

```Haskell
{-@ example0Q :: QueueN _ 0 @-} 
example0Q = Q nil nil
```

--------------------------------

### Example CSV Data with LiquidHaskell Types

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2013-10-10-csv-tables.lhs

An example of a CSV table representing menu items and prices, annotated with LiquidHaskell types to enforce constraints on string lengths and list structures.

```haskell
73: (CSV.CSV)zumbarMenu = x1:[[(GHC.Types.Char)]]
-> [{VV : [[(GHC.Types.Char)]] | ((len VV) == (len x1))}]
-> (CSV.CSV)Csv {VV : [{VV : [(GHC.Types.Char)] | ((len VV) >= 0)}]<_ VV -> ((len VV) >= 0)> | (((null VV)) <=> false) && ((len VV) >= 0)}[  {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Item"     , {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Price"]
74:                  [ {VV : [{VV : [(GHC.Types.Char)] | ((len VV) >= 0)}]<_ VV -> ((len VV) >= 0)> | (((null VV)) <=> false) && ((len VV) >= 0)}[{VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Espresso" , {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"2.25" ]  
75:                  , {VV : [{VV : [(GHC.Types.Char)] | ((len VV) >= 0)}]<_ VV -> ((len VV) >= 0)> | (((null VV)) <=> false) && ((len VV) >= 0)}[{VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Macchiato", {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"2.75" ]
76:                  , {VV : [{VV : [(GHC.Types.Char)] | ((len VV) >= 0)}]<_ VV -> ((len VV) >= 0)> | (((null VV)) <=> false) && ((len VV) >= 0)}[{VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Cappucino", {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"3.35" ]
77:                  , {VV : [{VV : [(GHC.Types.Char)] | ((len VV) >= 0)}]<_ VV -> ((len VV) >= 0)> | (((null VV)) <=> false) && ((len VV) >= 0)}[{VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Americano", {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"2.25" ]
78:                  ]
```

--------------------------------

### Proving Set Properties

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_08_Measure_Set.html

Examples of proving commutativity, associativity, and distributivity for set operations.

```haskell
{-@ prop_intersection_comm :: _ -> _ -> True @-}
prop_intersection_comm x y
= (x `intersection` y) == (y `intersection` x)
```

```haskell
{-@ prop_union_assoc :: _ -> _ -> _ -> True @-}
prop_union_assoc x y z
= (x `union` (y `union` z)) == (x `union` y) `union` z
```

```haskell
{-@ prop_intersection_dist :: _ -> _ -> _ -> True @-}
prop_intersection_dist x y z
= x `intersection` (y `union` z)
==
(x `intersection` y) `union` (x `intersection` z)
```

--------------------------------

### Create Valid ByteStrings

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_11_Case_Study_Pointers.html

Examples of constructing valid ByteStrings using the constructor with safe offsets and lengths.

```haskell
{-@ good1 :: IO (ByteStringN 5) @-}
good1 = do fp <- mallocForeignPtrBytes 5
return (BS fp 0 5)
```

```haskell
{-@ good2 :: IO (ByteStringN 2) @-}
good2 = do fp <- mallocForeignPtrBytes 5
return (BS fp 3 2)
```

--------------------------------

### GetOdds2 Type Signature and Implementation

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2014-08-15-a-finer-filter.lhs

Example of using filter2 to get odd integers. LiquidHaskell flags this as an error because it expects an `Odd` type but `filter2` instantiates `a` to `Int`, which is a supertype.

```haskell
181: {-@ getOdds2 :: [Int] -> [Odd] @-}
182: [Int] -> [{v : Int | ((v mod 2) == 1)}]getOdds2     = (x2:Int -> (Maybe {x13 : Int | (x13 == x2)}))
-> x3:[Int]
-> {x4 : [Int] | ((Set_sub (elts x4) (elts x3))) && ((len x4) >= 0) && ((len x4) <= (len x3))}filter2 x1:Int
-> (Maybe {x6 : Int | (x6 == x1) && (x6 == (x1  :  int)) && ((x6 mod 2) == 1) && (x6 /= 0)})isOdd
```

--------------------------------

### Build the tutorial project

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_01_Introduction.html

Commands to compile the project using Cabal or Stack.

```bash
cabal v2-build
```

```bash
stack build --fast --file-watch
```

--------------------------------

### GetEvens2 Type Signature and Implementation

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2014-08-15-a-finer-filter.lhs

Example of using filter2 to get even integers. LiquidHaskell flags this as an error because it expects an `Even` type but `filter2` instantiates `a` to `Int`, which is a supertype.

```haskell
178: {-@ getEvens2 :: [Int] -> [Even] @-}
179: [Int] -> [{v : Int | ((v mod 2) == 0)}]getEvens2    = (x2:Int -> (Maybe {x13 : Int | (x13 == x2)}))
-> x3:[Int]
-> {x4 : [Int] | ((Set_sub (elts x4) (elts x3))) && ((len x4) >= 0) && ((len x4) <= (len x3))}filter2 x1:Int
-> (Maybe {x5 : Int | (x5 == x1) && (x5 == (x1  :  int)) && ((x5 mod 2) == 0)})isEven
```

--------------------------------

### Clone the LiquidHaskell tutorial repository

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_01_Introduction.html

Use this command to download the tutorial source code.

```bash
git clone --recursive https://github.com/ucsd-progsys/liquidhaskell-tutorial.git
```

--------------------------------

### GetPoss2 Type Signature and Implementation

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2014-08-15-a-finer-filter.lhs

Example of using filter2 to get positive integers. LiquidHaskell flags this as an error because it expects a `Pos` type but `filter2` instantiates `a` to `Int`, which is a supertype.

```haskell
175: {-@ getPoss2 :: [Int] -> [Pos] @-}
176: [Int] -> [{v : Int | (0 < v)}]getPoss2     = (x2:Int -> (Maybe {x13 : Int | (x13 == x2)}))
-> x3:[Int]
-> {x4 : [Int] | ((Set_sub (elts x4) (elts x3))) && ((len x4) >= 0) && ((len x4) <= (len x3))}filter2 x1:Int
-> (Maybe {x6 : Int | (x6 == x1) && (x6 == (x1  :  int)) && (x6 > 0) && (0 < x6)})isPos
```

--------------------------------

### Initialize Refinement Reflection Module

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2016-09-18-refinement-reflection.lhs

Setup the module with necessary LiquidHaskell flags and imports for proof construction.

```haskell
38: {-@ LIQUID "--higherorder"     @-}
39: {-@ LIQUID "--totality"        @-}
40: module RefinementReflection where
41: import Language.Haskell.Liquid.ProofCombinators
42: 
43: fib :: Int -> Int
44: propPlusComm :: Int -> Int -> Proof 
45: propOnePlueOne :: () -> Proof 
46: fibTwo :: () -> Proof 
47: fibCongruence :: Int -> Int -> Proof
48: fibUp :: Int -> Proof 
49: fibTwoPretty :: Proof 
50: fibThree :: () -> Proof 
51: fMono :: (Int -> Int)
52:       -> (Int -> Proof)
53:       -> Int
54:       -> Int 
55:       -> Proof 
56: fibMono :: Int -> Int -> Proof 
57: 
```

--------------------------------

### Invalid Append Example

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2013-07-29-putting-things-in-order.lhs

An example of an append operation that does not result in an IncrList.

```haskell
499: [1,2,4] ++ [3,5,6]
```

--------------------------------

### Define Transposed Matrix Example

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_07_Measure_Int.html

Example of a transposed matrix structure.

```haskell
-- >>> ok32 == transpose ok23
-- True
ok32 = M 3 2 (V 3 [ V 2 [1, 4]
, V 2 [2, 5]
, V 2 [3, 6] ])
```

--------------------------------

### Liquid Haskell Module Setup

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2018-05-17-hillel-verifier-rodeo-I-leftpad.lhs

Sets up the Liquid Haskell module with necessary pragmas and imports. Includes type signatures for list operations and helper functions.

```haskell
{-@ LIQUID "--reflection"  @-}
```

```haskell
{-@ LIQUID "--ple"         @-}
```

```haskell
{-@ infixr ++              @-}
```

```haskell
{-@ infixr !!              @-}
```

```haskell
module PadLeft where
```

```haskell
import Prelude hiding (max, replicate, (++), (!!))
```

```haskell
(!!) :: [a] -> Int -> a
```

```haskell
size :: [a] -> Int
```

```haskell
(++) :: [a] -> [a] -> [a]
```

```haskell
obviously         :: Int -> a -> [a] -> ()
```

```haskell
replicate         :: Int -> a -> [a]
```

```haskell
thmReplicate      :: Int -> a -> Int -> ()
```

```haskell
thmAppLeft        :: [a] -> [a] -> Int -> ()
```

```haskell
thmAppRight       :: [a] -> [a] -> Int -> ()
```

```haskell
thmLeftPad        :: Int -> a -> [a] -> Int -> ()
```

--------------------------------

### Define Invalid Matrix Examples

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_07_Measure_Int.html

Examples of matrices that violate dimension constraints.

```haskell
bad1 :: Matrix Int
bad1 = M 2 3 (V 2 [ V 3 [1, 2 ]
, V 3 [4, 5, 6]])
bad2 :: Matrix Int
bad2 = M 2 3 (V 2 [ V 2 [1, 2]
, V 2 [4, 5] ])
```

--------------------------------

### Configure LiquidHaskell and Import Proof Combinators

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2016-10-06-structural-induction.lhs

Sets up the module with higher-order logic and totality checking enabled, and imports necessary proof combinators.

```haskell
46: {-@ LIQUID "--higherorder"     @-}
47: {-@ LIQUID "--totality"        @-}
48: module StructuralInduction where
49: import Language.Haskell.Liquid.ProofCombinators
50: 
51: import Prelude hiding (length)
52: 
53: length :: List a -> Int
54: leftId :: List a -> Proof
55: rightId :: List a -> Proof
56: associativity :: List a -> List a -> List a -> Proof
```

--------------------------------

### Invalid Implication Example

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_02_Logic.html

An example of a predicate that is not valid due to the use of the OR operator.

```haskell
{-@ ex3' :: Bool -> Bool -> TRUE @-}
ex3' a b = (a || b) ==> a
```

--------------------------------

### Vector Creation Examples

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_07_Measure_Int.html

Illustrates the creation of `Vector` instances. `okVec` is accepted by Liquid Haskell, while `badVec` is rejected due to a dimension mismatch.

```haskell
okVec = V 2 [10, 20] -- accepted by LH
```

```haskell
badVec = V 2 [10, 20, 30] -- rejected by LH
```

--------------------------------

### Example of Invalid Pointer Usage

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_11_Case_Study_Pointers.html

An example that triggers a LiquidHaskell error due to an out-of-bounds write.

```haskell
exBad = do fp <- mallocForeignPtrBytes 4
withForeignPtr fp $ \p -> do
poke (p `plusPtr` 0) zero
poke (p `plusPtr` 1) zero
poke (p `plusPtr` 2) zero
poke (p `plusPtr` 5) zero -- LH complains
return fp
where
zero = 0 :: Word8
```

--------------------------------

### Automating Proofs with PLE

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2017-12-24-splitting-and-splicing-intervals-II.lhs

Shows how to use Proof by Logical Evaluation (PLE) to automate proofs that would otherwise require manual equational steps.

```haskell
194: {-@ test1_ple :: () -> { S.member 2 (rng 1 3) } @-}
195: () -> {VV : () | Set_mem 2 (RangeSet.rng 1 3)}test1_ple () = ()
196: 
197: {-@ test2_ple :: () -> { S.member 2 (rng 0 3) } @-}
198: () -> {VV : () | Set_mem 2 (RangeSet.rng 0 3)}test2_ple () = ()
```

--------------------------------

### GHCi Evaluation Example

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_10_Case_Study_Associative_Maps.html

Example of an unsafe evaluation call that would lead to a runtime error.

```haskell
ghci> eval emp (Var "x")
```

--------------------------------

### Universal Quantifier Example

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2019-10-20-why-types.lhs

Illustrates a universally quantified logical formula that SMT solvers may struggle to instantiate effectively.

```logic
forall x. P(x)
```

--------------------------------

### Define a 2D Cluster Example

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2013-02-17-kmeans-clustering-II.lhs

Example of a 2-dimensional cluster represented as a list of points. Each point is a list of Doubles.

```haskell
exampleCluster = [ [0,  0]
                 , [1, 10]
                 , [2, 20]
                 , [4, 40]
                 , [5, 50] ]
```

--------------------------------

### Queue Construction Examples

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_09_Case_Study_Lazy_Queues.html

Illustrates valid and invalid Queue constructions based on the size invariant enforced by LiquidHaskell. `okQ` is accepted because |front| > |back|, while `badQ` is rejected because |front| < |back|.

```haskell
okQ = Q okList nil -- accepted, |front| > |back|
badQ = Q nil okList -- rejected, |front| < |back|
```

--------------------------------

### Example Usage of Ordered Lists

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_05_Datatypes.html

Demonstrates the creation of ordered and unordered lists using the refined `IncList` data type. `okList` is accepted, while `badList` is rejected by LiquidHaskell.

```Haskell
okList = 1 :< 2 :< 3 :< Emp -- accepted by LH
badList = 2 :< 1 :< 3 :< Emp -- rejected by LH
```

--------------------------------

### Example LiquidHaskell type error output

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_01_Introduction.html

An example of the error message displayed by GHC when a refinement type mismatch occurs.

```text
src/Tutorial_01_Introduction.lhs:30:27: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Int | v >= 0
                                && v == len xs}
    .
    is not a subtype of the required type
      VV : {VV : GHC.Types.Int | VV /= 0}
    .
    in the context
      xs : {v : [GHC.Types.Int] | len v >= 0}
   |
30 | average xs = sum xs `div` length xs
   |                           ^^^^^^^^^
```

--------------------------------

### Configure LiquidHaskell Options

Source: https://ucsd-progsys.github.io/liquidhaskell/options

Methods for passing configuration options to LiquidHaskell.

```haskell
{-@ LIQUID "--opt1" @-}
```

```text
ghc-options: -fplugin-opt=LiquidHaskell:--opt1 -fplugin-opt=LiquidHaskell:--opt2
```

```bash
LIQUIDHASKELL_OPTS="--opt1 --opt2"
```

```bash
liquid --opt1 --opt2 ...
```

--------------------------------

### Using Data.Map in Haskell

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_10_Case_Study_Associative_Maps.html

Demonstrates basic usage of Data.Map, including creating a map from a list and accessing elements. Note that accessing a non-existent key throws an exception.

```haskell
ghci> :m +Data.Map
ghci> let m = fromList [ ("haskell"   , "lazy")
                       , ("javascript", "eager")]

ghci> m ! "haskell"
"lazy"

ghci> m ! "python"
"*** Exception: key is not in the map
```

--------------------------------

### Example of a Unique List (UniqList)

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2013-07-29-putting-things-in-order.lhs

An example of a UniqList containing integers with no duplicate elements. This type alias guarantees that all elements in the list are distinct.

```haskell
{-@ noDuplicates :: UniqList Integer @-} 
noDuplicates = {VV : [{VV : (GHC.Integer.Type.Integer) | (VV > 0) && (0 <= VV) && (VV <= 9)}]<X VV -> (X /= VV) && (VV > 0) && (X >= VV) && (VV < X) && (0 <= VV) && (VV <= 9)> | (((null VV)) <=> false) && ((len VV) >= 0)}[1,3,2]
```

--------------------------------

### Example of a Decreasing List (DecrList)

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2013-07-29-putting-things-in-order.lhs

An example of a DecrList containing integers in decreasing order. This type alias ensures that each element is greater than or equal to the next.

```haskell
{-@ mustGoDown :: DecrList Integer @-} 
mustGoDown = {VV : [{VV : (GHC.Integer.Type.Integer) | (VV > 0) && (0 <= VV) && (VV <= 9)}]<X VV -> (VV == 1) && (X /= VV) && (VV > 0) && (X >= VV) && (VV < X)> | (((null VV)) <=> false) && ((len VV) >= 0)}[3,2,1]
```

--------------------------------

### Initialize LiquidHaskell Module

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2017-12-24-splitting-and-splicing-intervals-II.lhs

Standard configuration for a LiquidHaskell module, including flags for reflection and higher-order logic.

```haskell
42: {-@ LIQUID "--short-names"    @-}
43: {-@ LIQUID "--exact-data-con" @-}
44: {-@ LIQUID "--no-adt"         @-}
45: {-@ LIQUID "--higherorder"    @-}
46: {-@ LIQUID "--diff"           @-}
47: {-@ LIQUID "--ple"            @-}
48: 
49: module RangeSet where
50: 
51: import           Prelude hiding (min, max)
52: import           Language.Haskell.Liquid.NewProofCombinators
```

--------------------------------

### Example of an Increasing List (IncrList)

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2013-07-29-putting-things-in-order.lhs

An example of an IncrList containing integers in increasing order. This type alias enforces that each element is less than or equal to the next.

```haskell
{-@ whatGosUp :: IncrList Integer @-} 
whatGosUp = {VV : [{VV : (GHC.Integer.Type.Integer) | (VV > 0) && (0 <= VV) && (VV <= 9)}]<X VV -> (VV == (X + 1)) && (VV > 0) && (VV > X) && (0 <= VV) && (VV <= 9)> | (((null VV)) <=> false) && ((len VV) >= 0)}[1,2,3]
```

--------------------------------

### Create and access a map

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_01_Introduction.html

Shows how to create an associative key-value map using Data.Map and access its elements. Requires importing Data.Map.

```Haskell
ghci> :m +Data.Map 
ghci> let m = fromList [ ("haskell", "lazy")
                       , ("ocaml"  , "eager")]

ghci> m ! "haskell"
"lazy"
```

--------------------------------

### Degenerate CSV Data Example

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2013-10-10-csv-tables.lhs

An example of a CSV data structure that contains a degenerate row with an incorrect number of elements, which the refined type aims to prevent.

```haskell
(CSV.CSV)deg = x1:[[(GHC.Types.Char)]]
-> [{VV : [[(GHC.Types.Char)]] | ((len VV) == (len x1))}]
-> (CSV.CSV)Csv {VV : [{VV : [(GHC.Types.Char)] | ((len VV) >= 0)}]<_ VV -> ((len VV) >= 0)> | (((null VV)) <=> false) && ((len VV) >= 0)}[  {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Id", {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Name", {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Days"]
           [ {VV : [{VV : [(GHC.Types.Char)] | ((len VV) >= 0)}]<_ VV -> ((len VV) >= 0)> | (((null VV)) <=> false) && ((len VV) >= 0)}[{VV : [(GHC.Types.Char)]<_ VV -> false> | (((null VV)) <=> false) && ((len VV) >= 0)}"1" , {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Jan" , {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"31"]
           , {VV : [{VV : [(GHC.Types.Char)] | ((len VV) >= 0)}]<_ VV -> ((len VV) >= 0)> | (((null VV)) <=> false) && ((len VV) >= 0)}[{VV : [(GHC.Types.Char)]<_ VV -> false> | (((null VV)) <=> false) && ((len VV) >= 0)}"2" , {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Feb" , {VV : [{VV : (GHC.Types.Char) | false}]<_ VV -> false> | (((null VV)) <=> true) && ((len VV) == 0) && ((len VV) >= 0)}""]
           ]
```

--------------------------------

### Valid CSV Data Example

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2013-10-10-csv-tables.lhs

An example of a CSV data structure that conforms to the refined type, ensuring each row has the correct number of elements corresponding to the headers.

```haskell
(CSV.CSV)csvGood = x1:[[(GHC.Types.Char)]]
-> [{VV : [[(GHC.Types.Char)]] | ((len VV) == (len x1))}]
-> (CSV.CSV)Csv {VV : [{VV : [(GHC.Types.Char)] | ((len VV) >= 0)}]<_ VV -> ((len VV) >= 0)> | (((null VV)) <=> false) && ((len VV) >= 0)}[{VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Id", {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Name", {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Days"]
              [ {VV : [{VV : [(GHC.Types.Char)] | ((len VV) >= 0)}]<_ VV -> ((len VV) >= 0)> | (((null VV)) <=> false) && ((len VV) >= 0)}[{VV : [(GHC.Types.Char)]<_ VV -> false> | (((null VV)) <=> false) && ((len VV) >= 0)}"1", {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Jan", {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"31"]
              , {VV : [{VV : [(GHC.Types.Char)] | ((len VV) >= 0)}]<_ VV -> ((len VV) >= 0)> | (((null VV)) <=> false) && ((len VV) >= 0)}[{VV : [(GHC.Types.Char)]<_ VV -> false> | (((null VV)) <=> false) && ((len VV) >= 0)}"2", {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Feb", {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"28"]
              , {VV : [{VV : [(GHC.Types.Char)] | ((len VV) >= 0)}]<_ VV -> ((len VV) >= 0)> | (((null VV)) <=> false) && ((len VV) >= 0)}[{VV : [(GHC.Types.Char)]<_ VV -> false> | (((null VV)) <=> false) && ((len VV) >= 0)}"3", {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Mar", {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"31"]
              , {VV : [{VV : [(GHC.Types.Char)] | ((len VV) >= 0)}]<_ VV -> ((len VV) >= 0)> | (((null VV)) <=> false) && ((len VV) >= 0)}[{VV : [(GHC.Types.Char)]<_ VV -> false> | (((null VV)) <=> false) && ((len VV) >= 0)}"4", {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"Apr", {VV : [(GHC.Types.Char)] | ((len VV) >= 0)}"30"]
              ]
```

--------------------------------

### Define KMeans Module and Instances

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2013-02-17-kmeans-clustering-II.lhs

Initial module setup and type class instances for WrapType, including Eq and Ord implementations.

```haskell
30: {-# LANGUAGE ScopedTypeVariables, TypeSynonymInstances, FlexibleInstances #-}
31: 
32: module KMeans (kmeans, kmeansGen) where
33: 
34: import KMeansHelper
35: import Prelude              hiding      (zipWith)
36: import Data.List                        (sort, span, minimumBy)
37: import Data.Function                    (on)
38: import Data.Ord                         (comparing)
39: import Language.Haskell.Liquid.Prelude  (liquidAssert, liquidError)
40: 
41: instance (GHC.Classes.Eq (KMeans.WrapType [GHC.Types.Double] a))Eq (WrapType [Double] a) where
42:    (==) = x:{VV : [{VV : (GHC.Types.Double) | false}] | false} 
-> y:{VV : [{VV : (GHC.Types.Double) | false}] | false} 
-> {VV : (GHC.Types.Bool) | ((? Prop([VV])) <=> (x = y))}(==) ({VV : [{VV : (GHC.Types.Double) | false}] | false} 
 -> {VV : [{VV : (GHC.Types.Double) | false}] | false} 
 -> {VV : (GHC.Types.Bool) | false})
-> ({VV : (KMeans.WrapType {VV : [{VV : (GHC.Types.Double) | false}] | false} {VV : a | false}) | false} 
    -> {VV : [{VV : (GHC.Types.Double) | false}] | false})
-> {VV : (KMeans.WrapType {VV : [{VV : (GHC.Types.Double) | false}] | false} {VV : a | false}) | false} 
-> {VV : (KMeans.WrapType {VV : [{VV : (GHC.Types.Double) | false}] | false} {VV : a | false}) | false} 
-> {VV : (GHC.Types.Bool) | false}`on` (KMeans.WrapType {VV : [{VV : (GHC.Types.Double) | false}] | false} {VV : a | false}) 
-> {VV : [{VV : (GHC.Types.Double) | false}] | false}getVect
43: 
44: instance (GHC.Classes.Ord (KMeans.WrapType [GHC.Types.Double] a))Ord (WrapType [Double] a) where
45:     compare = (GHC.Classes.Ord [GHC.Types.Double])comparing (KMeans.WrapType {VV : [{VV : (GHC.Types.Double) | false}] | false} {VV : a | false}) 
-> {VV : [{VV : (GHC.Types.Double) | false}] | false}getVect
```

--------------------------------

### QuickSort Implementation Stub

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_07_Measure_Int.html

This is a stub for the `quickSort` function, intended to be implemented using the `partition` function. The provided test case demonstrates its expected usage.

```Haskell
-- >> quickSort [1,4,3,2]
-- [1,2,3,4]
{-@ quickSort :: (Ord a) => xs:List a -> ListX a xs @-}
quickSort [] = []
quickSort (x:xs) = undefined
{-@ test10 :: ListN String 2 @-}
test10 = quickSort (drop 1 ["cat", "dog", "mouse"])
```

--------------------------------

### Automatic Specification Loading Example

Source: https://ucsd-progsys.github.io/liquidhaskell/options

Liquid Haskell automatically loads specifications from modules named `_LHAssumptions` when an import is encountered. For example, an import of `Data.Vector` triggers a search for `Data.Vector_LHAssumptions`.

```haskell
import Data.Vector
import Data.Vector.Unboxed
```

--------------------------------

### Bounded Addition Exercise

Source: https://ucsd-progsys.github.io/liquidhaskell-tutorial/Tutorial_08_Measure_Set.html

Template for proving the bounded addition theorem.

```haskell
{-@ prop_x_y_200 :: _ -> _ -> True @-}
prop_x_y_200 x y = False -- fill in the theorem body
```

--------------------------------

### SList Destruction API

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2015-01-30-okasakis-lazy-queue.lhs

Provides functions to deconstruct SLists: `hd` to get the first element and `tl` to get the rest of the list. These functions are safe to use only on non-empty lists.

```APIDOC
## SList Destruction

### `hd`

#### Description
Returns the first element of a non-empty SList.

#### Type Signature
```hcl
{-@ hd :: xs:NEList a -> a @-}
```

#### Implementation
```hcl
hd (SL _ (x:_)) = x
```

### `tl`

#### Description
Returns the SList without its first element. The size of the resulting list is one less than the original.

#### Type Signature
```hcl
{-@ tl :: xs:NEList a -> SListN a {size xs - 1} @-}
```

#### Implementation
```hcl
tl (SL n (_:xs)) = SL (n - 1) xs
```
```

--------------------------------

### LiquidHaskell Default Termination Proof Example

Source: https://ucsd-progsys.github.io/liquidhaskell/specifications

An example of a function 'append' that terminates. LiquidHaskell uses the default termination metric 'llen' defined for the 'L' type to automatically prove its termination.

```haskell
append :: L a -> L a -> L a  
append N           ys = ys
append (Cons x xs) ys = Cons x (append xs ys)
```

--------------------------------

### Initial Quick Sort Attempt

Source: https://ucsd-progsys.github.io/liquidhaskell/blogposts/2013-07-29-putting-things-in-order.lhs

A standard Quick Sort implementation that fails verification due to the type constraints of the append operator.

```haskell
481: {-@ quickSort'    :: (Ord a) => [a] -> IncrList a @-}
482: quickSort' []     = []
483: quickSort' (x:xs) = lts ++ (x : gts) 
484:   where 
485:     lts           = quickSort' [y | y <- xs, y < x]
486:     gts           = quickSort' [z | z <- xs, z >= x]
```

--------------------------------

### Liquid Type Mismatch Error Example

Source: https://ucsd-progsys.github.io/liquidhaskell/options

This is an example of a type mismatch error reported by LiquidHaskell when the `--counter-examples` flag is enabled. It shows the inferred type, the required type, and the context.

```haskell
tests/neg/ListElem.hs:12:1-8: Error: Liquid Type Mismatch

 12 | listElem _ []      = False
      ^^^^^^

   Inferred type
     VV : {VV : Bool | VV == True}
     VV = True

   not a subtype of Required type
     VV : {VV : Bool | VV <=> Set_mem ?b (listElts ?a)}

   In Context
     ?a : {?a : [a] | len ?a >= 0}
     ?a = [1]

     ?b : a
     ?b = 0
```
Tokens:
Raw