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

[Conal Elliott]

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 <hans at 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
>
>  -
>
> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140705/4c4b6e09/attachment.html>