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.
If you haven't already, see *Denotational design with type class morphisms
http://conal.net/papers/type-class-morphisms* for principles and examples.
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.
Good luck!
-- Conal
http://conal.net/papers/type-class-morphisms
On Fri, Jul 4, 2014 at 4:49 PM, Hans Höglund
Dear all,
This may seem a strange question due to my unfamiliarity with formal semantics, but bear with me.
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
type Duration = Double type Time = Point Duration type Span = Time^2 type Note a = (Span, a)
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.
My question is basically:
1) Is my approach (using pseudo-Haskell) a sound way to state denotational semantics? 2) How can I state semantics (in code and/or documentation), and be sure that my implementation follow the semantics?
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?
Sincerly, Hans
-
Hans Höglund *Composer, conductor and developer*
hans [at] hanshoglund.se hanshoglund.com https://twitter.com/hanshogl https://soundcloud.com/hanshoglund http://github.com/hanshoglund
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe