[Haskell-cafe] Haskell Propeganda

Neil Mitchell ndmitchell at gmail.com
Thu Aug 28 20:02:08 EDT 2008


Hi

> Tools like Neil Mitchell's Catch can do more sophisticated checking, as long
> as your program can be compiled by YHC. Sometimes fromJust can be quite
> useful, though, especially in tandem with isJust. For example,
>
>> prop_foobar :: SomeType -> Property
>> prop_foobar x
>>  = isJust (someTypeToMaybe x) ==> fromJust x == expectedResult

I was thinking of jumping in on this thread, to advertise Catch, but
unfortunately "can be compiled with Yhc" makes it a fairly niche tool
:-(  However, the fundamental bit of Catch works on an a normal Core
language, and I do want to hook it up to GHC's Core language at some
point. It could certainly deal with prop_foobar, and things that are
far more complex.

To get an idea of what Catch can do, I recommend reading the draft
paper and skipping to section 5.4 where I verify the entire HsColour
program with one small refactoring and no annotations. I even found 3
real crashing bugs in HsColour, that were fixed because Catch pointed
them out. Incomplete patterns + a checker (Catch) are just a faster
and more efficient way of writing complete patterns without dead code
:-)

Catch: http://www-users.cs.york.ac.uk/~ndm/catch/

Thanks

Neil


More information about the Haskell-Cafe mailing list