Generally the way this is done in Haskell is that the interface to the type
is specified in a typeclass (or, alternatively, in a module export list,
for concrete types), and the axioms are specified in a method to be tested
in some framework (i.e. QuickCheck, SmallCheck, SmartCheck) which can
automatically generate instances of your type and test that the axioms hold.
For example:
class QueueLike q where
empty :: q a
insert :: a -> q a -> q a
viewFirst :: q a -> Maybe (a, q a)
size :: q a -> Integer
-- can use a single proxy type if have kind polymorphism, but that's an
experimental feature right now
data Proxy2 (q :: * -> *) = Proxy2
instance Arbitrary (Proxy2 q) where arbitrary = return Proxy2
prop_insertIncrementsSize :: forall q. QueueLike q => q () -> Bool
prop_insertIncrementsSize q = size (insert () q) == size q + 1
prop_emptyQueueIsEmpty :: forall q. QueueLike q => Proxy2 q => Bool
prop_emptyQueueIsEmpty Proxy2 = maybe True (const False) $ view (empty :: q
())
Then you specialize these properties to your type and test them:
instance QueueLike [] where ...
ghci> quickCheck (prop_insertIncrementsSize :: [()] -> Bool)
Valid, passed 100 tests
or
Failed with: [(), (), ()]
QuickCheck randomly generates objects of your data structure and tests your
property against them. While not as strong as a proof, programs with 100%
quickcheck coverage are *extremely* reliable. SmartCheck is an extension
of QuickCheck that tries to reduce test cases to the minimum failing size.
SmallCheck does exhaustive testing on the properties for finite data
structures up to a particular size. It's quite useful when you can prove
your algorithms 'generalize' after a particular point.
There aren't any libraries that I know of for dependent-type style program
proof for haskell; I'm not sure it's possible. The systems I know of have
you program in a more strongly typed language (Coq/agda) and export Haskell
programs once they are proven safe. Many of these rely on unsafeCoerce in
the Haskell code because they have proven stronger properties about the
types than Haskell can; I look at that code with some trepidation--I am not
sure what guarantees the compiler makes about unsafeCoerce.
-- ryan
On Sun, Jul 22, 2012 at 7:19 AM, Patrick Browne <patrick.bro...@dit.ie>wrote:
> {-
> Below is a *specification* of a queue.
> If possible I would like to write the equations in type class.
> Does the type class need two type variables?
> How do I represent the constructors?
> Can the equations be written in the type class rather than the instance?
> -}
>
> module QUEUE_SPEC where
> data Queue e = New | Insert (Queue e) e deriving Show
>
> isEmpty :: Queue e -> Bool
> isEmpty New = True
> isEmpty (Insert q e) = False
>
> first :: Queue e -> e
> first (Insert q e) = if (isEmpty q) then e else (first q)
>
>
> rest :: Queue e -> Queue e
> rest (Insert q e ) = if (isEmpty q) then New else (Insert (rest q) e)
>
>
> size :: Queue e -> Int
> size New = 0
> size (Insert q e) = succ (size q)
>
> {-
> some tests of above code
> size (Insert (Insert (Insert New 5) 6) 3)
> rest (Insert (Insert (Insert New 5) 6) 3)
>
> My first stab at a class
> class QUEUE_SPEC q e where
> new :: q e
> insert :: q e -> q e
> isEmpty :: q e -> Bool
> first :: q e -> e
> rest :: q e -> q e
> size :: q e -> Int
>
> -}
>
>
> Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís
> Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a
> bheith slán. http://www.dit.ie
> This message has been scanned for content and viruses by the DIT
> Information Services E-Mail Scanning Service, and is believed to be clean.
> http://www.dit.ie
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
