[Haskell-cafe] How to state semantics in denotational design?

[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




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140705/c6ae996f/attachment.html>