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 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