Hi,
Thanks for all the very useful feed back on this thread.
I would like to present my possibly incorrect summarized view:
Class signatures can contain placeholders for constructors.
These place-holder-constructors cannot be used in the class to define functions (I assume other in-scope constructors can be used).
In the instance a real constructor can be substituted for the place-holder-constructor.
Does this restrict the type of equation that can be used in a type class?
It seems that some equations respecting the constructor discipline are not allowed.
I appreciate that in Haskell the most equations occur in the instances, but from my earlier post:
"I merely wish to identify the strengths and weakness of *current Haskell type classes* as a pure *unit of specification*"
Is my summarized view is correct?
Regards,
Pat
On 31/07/12, Ryan Ingram <ryani.s...@gmail.com> wrote:
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.
-- ryanOn Sun, Jul 22, 2012 at 7:19 AM, Patrick Browne <patrick.bro...@dit.ie <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 <Haskell-Cafe@haskell.org>
http://www.haskell.org/mailman/listinfo/haskell-cafe
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
