<div dir="ltr"><div><div>Hi Hans. I assume you have more data types, such as scores. Defining semantics/models for those types would be the heart of a denotational design, along with the meanings of every element of your API in terms of these models/semantics. For any type class instances you have, the principle of type class morphisms will usually determine the meanings of those instances, and often one can derive/calculate implementations from those determined meanings.</div>

<div><br></div>If you haven't already, see <i><a href="http://conal.net/papers/type-class-morphisms">Denotational design with type class morphisms</a></i> for principles and examples.<br><br>I don't know how to keep the calculations & 
proofs in sync with changes to the specification, using Haskell. Maybe 
you could use a proof assistant environment, but I'm guessing. As you suggested, QuickCheck could also help, especially since using denotational design means that you have a precise specification.<br></div><div><br>Good luck!<br>

<br></div><div>-- Conal<br></div><div><a href="http://conal.net/papers/type-class-morphisms"></a><div><div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Jul 4, 2014 at 4:49 PM, Hans Höglund <span dir="ltr"><<a href="mailto:hans@hanshoglund.se" target="_blank">hans@hanshoglund.se</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="word-wrap:break-word"><div>Dear all,</div><div><br></div><div>This may seem a strange question due to my unfamiliarity with formal semantics, but bear with me.</div>

<div><br></div><div>I am trying to apply denotational design principles to my library music-score, and often find myself writing down semantics of data structures in pseudo-Haskell such as</div><div><br></div><div>> type Duration = Double</div>

<div>> type Time = Point Duration</div><div>> type Span = Time^2</div><div>> type Note a = (Span, a)</div><div><br></div><div>The actual implementation of the data structures may or may not be identical to the semantics. For example, it makes sense to implement Span as (Time^2) or (Time x Duration), as these types are isomorphic.</div>

<div><br></div><div>My question is basically:</div><div><br></div><div>1) Is my approach (using pseudo-Haskell) a sound way to state denotational semantics?</div><div>2) How can I state semantics (in code and/or documentation), and be sure that my implementation follow the semantics?</div>

<div><br></div><div>I understand that the correctness of the implementation w.r.t. to the semantics can be verified using manual proofs, which worries me as I want to be able to refactor the semantics and be make sure that the implementation is still correct without having to repeat all the proofs. Is there a "trick" to encode the semantics in actual Haskell and have the type system and/or QuickCheck do the verification for me? Or am I misunderstanding the concept of denotational design?</div>

<div><br></div><div>Sincerly,</div><div>Hans</div><div><br></div><div>
<span style="border-collapse:separate;color:rgb(0,0,0);font-family:Helvetica;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;font-size:medium"><span style="border-collapse:separate;color:rgb(0,0,0);font-family:Helvetica;font-style:normal;font-variant:normal;font-weight:normal;letter-spacing:normal;line-height:normal;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;font-size:medium"><div style="word-wrap:break-word">

<div>-</div><div><br></div><div>Hans Höglund</div><div><i>Composer, conductor and developer</i></div><div><br></div><div>hans [at] <a href="http://hanshoglund.se" target="_blank">hanshoglund.se</a></div><div><div><a href="http://hanshoglund.com" target="_blank">hanshoglund.com</a></div>

<div><div><div><a href="https://twitter.com/hanshogl" target="_blank">https://twitter.com/hanshogl</a></div></div></div><div><a href="https://soundcloud.com/hanshoglund" target="_blank">https://soundcloud.com/hanshoglund</a></div>

<div><a href="http://github.com/hanshoglund" target="_blank">http://github.com/hanshoglund</a></div><div><br></div></div></div></span><br></span><br>
</div>
<br></div><br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><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></div></div></div></div>