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 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


On Fri, Jul 4, 2014 at 4:49 PM, Hans Höglund <hans@hanshoglund.se> wrote:
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



_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe