Changelog History
Page 2

v0.6.0.0
April 05, 2016 
v0.5.0.1
 ๐ Fixed a bug in the specification for
Data.Traversable.sequence
 0๏ธโฃ Make interpreted mul and div the default, when
solver = z3
 ๐ Use
higherorder
to allow higher order binders into the fixpoint environment
 ๐ Fixed a bug in the specification for

v0.5.0.0
โ Added support for building with
stack
โ Added support for GHC 7.10 (in addition to 7.8)
โ Added 'cabaldir' option that will automatically find a .cabal file in the ancestor path from which the target file belongs, and then add the relevant source and dependencies to the paths searched for by LiquidHaskell.
This means we don't have to manually do
i src
etc. when checking large projects, which can be tedious e.g. within emacs. 
v0.4.0.0
 ๐ Bounds as an alternative for logical constraints see
benchmarks/icfp15/pos/Overview.lhs
 ๐ Bounds as an alternative for logical constraints see

v0.3.0.0
Logical constraints: add extra subtyping constraints to signatures, e.g.
{[email protected] (.) :: forall c > Prop, q :: a > b > Prop, r :: a > c > Prop>. {x::a, w::b  c <: c} (y:b > c) > (z:a > b) > x:a > c @} (.) f g x = f (g x)
Inlining haskell functions as predicates and expressions, e.g.
{[email protected] inline max @} max x y = if x >= y then x else y
Refining class instances. For example
{[email protected] instance Compare Int where cmax :: Odd > Odd > Odd @}
Major restructuring of internal APIs

v0.2.1.0
 ๐ Experimental support for lifting haskell functions to measures
If you annotate a Haskell function
foo
with {[email protected] measure foo @}, LiquidHaskell will attempt to derive an equivalent measure fromfoo
's definition. This should help eliminate some boilerplate measures that used to be required.
 ๐ Experimental support for lifting haskell functions to measures
If you annotate a Haskell function

v0.2.0.0
๐ Move to GHC7.8.3 LiquidHaskell now requires ghc7.8.3.
Termination ๐ LiquidHaskell will now attempt to prove all recursive functions terminating. It tries to prove that some parameter (or combination thereof) decreases at each recursive callsite. By default, this will be the first parameter with an associated size measure (see Size Measures), but can be overridden with the
Decreases
annotation or a termination expression (see Termination Expressions).
If proving termination is too big of burden, it can be disabled on a permodule basis with the
notermination
flag, or on a perfunction basis with theLazy
annotation.Size Measures Data declarations now optionally take a size measure, which LiquidHaskell will use to prove termination of recursive functions. The syntax is:
{[email protected] data List a [len] = Nil  Cons a (List a) @}
Termination Expressions Termination Expressions can be used to specify the decreasing metric of a recursive function. They can be any valid LiquidHaskell expression and must be placed after the function's LiquidHaskell type, e.g.
{[email protected] map :: (a > b) > xs:[a] > [a] / [len xs] @}
Type Holes To reduce the annotation burden, LiquidHaskell now accepts
_
as a placeholder for types and refinements. It can take the place of any base Haskell type and LiquidHaskell will query GHC to fill in the blanks, or it can take the place of a refinement predicate, in which case LiquidHaskell will infer an appropriate refinement. For example,{[email protected] add :: x:_ > y:_ > {v:_  v = x + y} @} add x y = x + y
becomes
{[email protected] add :: Num a => x:a > y:a > {v:a  v = x + y} @} add x y = x + y
Assumed Specifications The
assume
annotation now works as you might expect it to, i.e. LiquidHaskell will not verify that the implementation is correct. Furthermore,assume
can be used to locally override the type of an imported function.Derived Measure Selectors Given a data definition
{[email protected] data Foo = Foo { bar :: Int, baz :: Bool } @}
LiquidHaskell will automatically derive measures
{[email protected] measure bar :: Foo > Int @} {[email protected] measure baz :: Foo > Bool @}
TypeClass Specifications LiquidHaskell can now verify prove that typeclass instances satisfy a specification. Simply use the new
class
annotation{[email protected] class Num a where (+) :: x:a > y:a > {v:a  v = x + y} () :: x:a > y:a > {v:a  v = x  y} ... @}
and LiquidHaskell will attempt to prove at each instance declaration that the implementations satisfy the class specification.
๐ When defining typeclass specifications you may find the need to use overloaded measures, to allow for typespecific definitions (see TypeIndexed Measures).
TypeIndexed Measures LiquidHaskell now accepts measures with typespecific definitions, e.g. a measure to describe the size of a value. Such measures are defined using the
class measure
syntax{[email protected] class measure size :: forall a. a > Int @}
and instances can be defined using the
instance measure
syntax, which mirrors the regular measure syntax{[email protected] instance measure size :: [a] > Int size ([]) = 0 size (x:xs) = 1 + size xs @} {[email protected] instance measure size :: Tree a > Int size (Leaf) = 0 size (Node l x r) = 1 + size l + size r @}
๐ Parsing ๐ We have greatly improved our parser to require fewer parentheses! Yay!
๐ Emacs/Vim Support LiquidHaskell now comes with syntax checkers for flycheck in Emacs and syntastic in Vim.
Incremental Checking LiquidHaskell has a new
diffcheck
flag that will only check binders that have changed since the last run, which can drastically improve verification times.๐ Experimental Support for Z3's theory of real numbers with the
real
flag.