True
is a bad argument10
is a good argumenttake
and drop
reconstruction0
fib
is an uninterpreted function0
average
take
fib
fib
is an uninterpreted functionList
s Elementsappend
take
and drop
reconstructiontake
and drop
reconstruction
Question: Is psum
equivalent to sum
?
plus
{-@ sumDistr :: xs:List Int -> ys:List Int ->
{sum (xs ++ ys) == plus (sum xs) (sum ys)} @-}
{-@ plusRightId :: xs:List Int ->
{plus (sum xs) (sum N) == sum xs} @-}
If f is right-id and op distributes ...
... then it is OK to map-reduce.
Lets prove Right Identity
Prove crucial properties for Haskell in Haskell!
where Haskell = a general purspose programming language.
cabal install liquidhaskell
https://github.com/ucsd-progsys/liquidhaskell
http://www.refinement-types.org
online demo @ http://goto.ucsd.edu/liquidhaskell
Built-in Lists are not supported for now.
(So does imports...)