<div style="font-family: 'Times New Roman'; font-size: 16px;"><br />Hi,<br _moz_dirty="" />Thanks for all the very useful feed back on this thread.<br _moz_dirty="" />I would like to present my possibly incorrect summarized  view:<br _moz_dirty="" />Class signatures can contain placeholders for constructors.<br _moz_dirty="" />These place-holder-constructors cannot be used in the class to define functions (I assume other in-scope constructors can be used). <br _moz_dirty="" />In the instance a real constructor can be substituted for the place-holder-constructor.<br _moz_dirty="" />Does this restrict the type of equation that can be used in a type class? <br _moz_dirty="" />It seems that some equations respecting the constructor discipline are not allowed.<br _moz_dirty="" /><br _moz_dirty="" />I appreciate that in Haskell the most equations occur in the instances, but from my earlier post:<br _moz_dirty="" /> &quot;I merely wish to identify the strengths and weakness of *current Haskell type classes* as a pure *unit of specification*&quot;<br _moz_dirty="" /> <br _moz_dirty="" />Is my summarized view is correct?<br _moz_dirty="" />Regards,<br _moz_dirty="" />Pat<br _moz_dirty="" /> <br /><span>On 31/07/12, <b class="name">Ryan Ingram </b> &lt;ryani.spam@gmail.com&gt; wrote:</span><blockquote cite="mid:CA+XKtKh20znrMnefGFhTGRu+2F4fkvFzUhiGMu_xWW930XCDSQ@mail.gmail.com" class="iwcQuote" style="border-left: 1px solid #00F; padding-left: 13px; margin-left: 0;" type="cite"><div class="mimepart text html">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.<br />
<br />For example:<br /><br />class QueueLike q where<br />    empty :: q a<br />    insert :: a -&gt; q a -&gt; q a<br />    viewFirst :: q a -&gt; Maybe (a, q a)<br />    size :: q a -&gt; Integer<br /><br />-- can use a single proxy type if have kind polymorphism, but that's an experimental feature right now<br />
data Proxy2 (q :: * -&gt; *) = Proxy2<br />instance Arbitrary (Proxy2 q) where arbitrary = return Proxy2<br /><br />prop_insertIncrementsSize :: forall q. QueueLike q =&gt; q () -&gt; Bool<br />prop_insertIncrementsSize q = size (insert () q) == size q + 1<br />
<br />prop_emptyQueueIsEmpty :: forall q. QueueLike q =&gt; Proxy2 q =&gt; Bool<br />prop_emptyQueueIsEmpty Proxy2 = maybe True (const False) $ view (empty :: q ())<br /><br />Then you specialize these properties to your type and test them:<br />
<br />instance QueueLike [] where ...<br /><br />ghci&gt; quickCheck (prop_insertIncrementsSize :: [()] -&gt; Bool)<br />Valid, passed 100 tests<br />or<br />Failed with: [(), (), ()]<br /><br />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.<br />
<br />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.<br /><br />
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.<br />
<br />  -- ryan<br /><br /><div class="gmail_quote">On Sun, Jul 22, 2012 at 7:19 AM, Patrick Browne <span dir="ltr">&lt;patrick.browne@dit.ie &lt;patrick.browne@dit.ie&gt;&gt;</span> wrote:<br /><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
{-<br />Below is a *specification* of a queue. <br />If possible I would like to write the equations in type class.<br />Does the type class need two type variables? <br />How do I represent the constructors?<br />Can the equations be written in the type class rather than the instance?<br />
-}<br /><br />module QUEUE_SPEC where<br />data Queue e   = New | Insert (Queue e) e deriving Show<br /><br />isEmpty :: Queue  e  -&gt; Bool<br />isEmpty  New  = True <br />isEmpty (Insert q e) = False <br /><br />first :: Queue  e  -&gt; e<br />
first (Insert q e) =  if (isEmpty q) then e else (first q) <br /><br /><br />rest :: Queue  e  -&gt; Queue  e<br />rest (Insert  q e ) = if (isEmpty q) then New  else (Insert (rest q) e)<br /><br /><br />size :: Queue  e  -&gt; Int<br />
size New  = 0 <br />size (Insert q e) = succ (size q)<br /><br />{- <br />some tests of above code<br />size (Insert (Insert (Insert New 5) 6) 3)<br />rest (Insert (Insert (Insert New 5) 6) 3)<br /><br />My first stab at a class<br />class QUEUE_SPEC q e where<br />
 new :: q e<br /> insert :: q e -&gt; q e<br /> isEmpty :: q  e  -&gt; Bool<br /> first :: q  e  -&gt; e<br /> rest :: q  e  -&gt; q e<br /> size :: q e  -&gt; Int<br /><br />-}<br /><br />
<br clear="all" /> 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.  <a href="http://www.dit.ie" target="_blank">http://www.dit.ie</a><br />


This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean.  <a href="http://www.dit.ie" target="_blank">http://www.dit.ie</a>



<br />_______________________________________________<br />
Haskell-Cafe mailing list<br />
Haskell-Cafe@haskell.org &lt;Haskell-Cafe@haskell.org&gt;<br />
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br />
<br /></blockquote></div><br />
</div></blockquote></div>
<br clear=all> 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.  <a href="http://www.dit.ie">http://www.dit.ie</a><br>
This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean.  <a href="http://www.dit.ie">http://www.dit.ie</a>