Changelog for liquidhaskell-0.8.0.0

Changes

NEXT

0.5.0.1

0.5.0.0

0.4.0.0

0.3.0.0

0.2.1.0

0.2.0.0

If proving termination is too big of burden, it can be disabled on a per-module basis with the --no-termination flag, or on a per-function basis with the Lazy annotation.

becomes

{-@ add :: Num a => x:a -> y:a -> {v:a | v = x + y} @-}
add x y = x + y

LiquidHaskell will automatically derive measures

{-@ measure bar :: Foo -> Int @-}
{-@ measure baz :: Foo -> Bool @-}

and LiquidHaskell will attempt to prove at each instance declaration that the implementations satisfy the class specification.

When defining type-class specifications you may find the need to use overloaded measures, to allow for type-specific definitions (see Type-Indexed Measures).

and instances can be defined using the instance measure syntax, which mirrors the regular measure syntax

{-@ instance measure size :: [a] -> Int
    size ([])   = 0
    size (x:xs) = 1 + size xs
  @-}
{-@ instance measure size :: Tree a -> Int
    size (Leaf)       = 0
    size (Node l x r) = 1 + size l + size r
  @-}