<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><br></div><div>Yes, this is indeed the point. Right now we express properties that a type class should obey, but there is no compiler assistance to prove or verify them.</div><div><br></div><div>A compiler aware of "properties" can do additional symbolic manipulation to increase performance. Surely there has been some research in this area already.</div><br><div apple-content-edited="true"> <span class="Apple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0; "><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><span class="Apple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; "><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><span class="Apple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; "><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><span class="Apple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; "><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><div>Regards,</div><div><br></div><div>John A. De Goes</div><div>N-BRAIN, Inc.</div><div>The Evolution of Collaboration</div><div><br></div><div><a href="http://www.n-brain.net">http://www.n-brain.net</a> | 877-376-2724 x 101</div></div></div></span></div></span></div></span></div></span> </div><br><div><div>On Feb 19, 2009, at 3:35 AM, Alberto G. Corona wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><br><br><div class="gmail_quote">2009/2/19 Wolfgang Jeltsch <span dir="ltr"><<a href="mailto:g9ks157k@acme.softbase.org">g9ks157k@acme.softbase.org</a>></span><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"> Am Donnerstag, 19. Februar 2009 02:22 schrieb sylvain:<br> <div class="Ih2E3d">> Haskell is a nice, mature and efficient programming language.<br> > By its very nature it could also become a nice executable formal<br> > specification language, provided there is tool support.<br> <br> </div>Wouldn't it be better to achieve the goals you describe with a dependently<br> typed programming language?<br></blockquote><div><br></div><div>But I wonder how a dependent typed language can express certain properties, for example, the distributive property between the operation + and * in a ring or simply the fact that show(read x)==x. As far as I understand, a dependent type system can restrict the set of values for wich a function apply, but it can not express complex relationships between operations. My knowledge on dependent types is very limited. I would like to be wrong on this.</div> <div><br></div><div>The point is that permits the automatic checking of such properties at the class level (or module level) are critical, to make sure that derived instances agree with that. This would be very good to feel confident and program at higuer levels of abstraction.</div> <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><br></blockquote></div> _______________________________________________<br>Haskell-Cafe mailing list<br><a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>http://www.haskell.org/mailman/listinfo/haskell-cafe<br></blockquote></div><br></body></html>