30

I've read a bit on denotational semantics (DS) and I'm very intrigued about the process of designing computer programs where types and functions have strong and clear mappings to mathematics.

Are there any resources that discuss designing programs based on DS in detail? I've seen a few superficial treatments of the subject.

I'm conversant in Haskell, Scala, Common Lisp, and a bit of Scheme so any resources that use those languages would be greatly appreciated.

Tim Stewart
  • 403
  • 4
  • 6
  • 7
    You should check out the work by Conal Elliott: http://conal.net –  Jan 16 '13 at 00:16
  • 2
    Curry-Howard isomorphism is the keyword, if you didn't know already. – pedrofurla Jan 16 '13 at 02:28
  • 2
    I thought a similar thing. I tried to design numerical simulation of points, rigid bodies and fluid. This (https://github.com/takagi/SimulationDSL) is one of my experiment in which I expressed vector algebra and partial equations in Haskell DSL. I also checked Conal Elliott's work. –  Jan 16 '13 at 02:55
  • 3
    You should check out [LtU](http://lambda-the-ultimate.org). There are probably some good old discussions there, or at least your question would be a better fit there than on SO –  Jan 16 '13 at 16:00
  • 3
    You might want to read Samuel Kamin's "An implementation-oriented semantics of Wadler's pretty-printing combinators". It compares operational and denotational approaches to implementing a well known, real world example and includes advocacy for a denotational approach. – stephen tetley Jan 16 '13 at 17:31
  • I sounds like Simon Peyton Jones' (et al.) paper about composing contracts also falls under the category of DS. – Tim Stewart Jan 17 '13 at 03:24
  • @stephentetley, I'm only a few paragraphs into Samuel Kamin's paper but it already sounds very promising. Thanks! The PostScript version (http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.55.2153&rep=rep1&type=ps) looks a lot nicer than the PDF on my Linux laptop. – Tim Stewart Jan 17 '13 at 03:32
  • When I was looking into FRP, I thought there were some very good examples of denotational semantics making my life simpler--I found behaviors and events far easier to understand and think about after seeing the denotational semantics for them. However, this is a *very* simple example, so I'm not sure how illustrative it would be. – Tikhon Jelvis Jan 17 '13 at 06:18
  • David A. Schmidt's book, "Denotational Semantics" has been very informative. It's available online for free at: http://www.scss.tcd.ie/Andrew.Butterfield/Teaching/CS4003/DenSem-full-book.pdf – Tim Stewart Feb 10 '13 at 05:23
  • concerning common lisp a look at [ACL2](http://www.cs.utexas.edu/~moore/acl2/) might be interesting for you Patrick –  Jan 18 '13 at 18:04

2 Answers2

14

Denotational design (program design rooted in and flowing from denotational semantics) is my primary methodology. A few years ago while writing about FRP, I got much clearer about what I'd been doing. See Push-pull functional reactive programming. For a more explicit description of the paradigm and a variety of examples, see Denotational design with type class morphisms. Once I became conscious of the pattern, I started looking for it everywhere. Where it fails, I know I have an abstraction leak. For an early, informal description, see Luke Palmer's blog post Semantic Design.

I'm always interested in applications of denotational design, so I'd love to hear about your explorations.

Conal
  • 256
  • 2
  • 4
7

We have applied denotational semantics to language design itself, arguing that the design of languages, in particular, domain-specific languages, should start with the definition of the semantics. If you are interested in the details, you might want to take a look at Semantics-Driven DSL Design and Semantics First! Rethinking the Language Design Process.

Martin Erwig
  • 71
  • 1