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