Применение денотационной семантики для проектирования программ

30

Я читал немного о денотационной семантике (DS), и я очень заинтригован процессом разработки компьютерных программ, где типы и функции имеют четкое и ясное отображение в математике.

Существуют ли какие-либо ресурсы, которые подробно обсуждают вопросы разработки программ на основе DS? Я видел несколько поверхностных обработок предмета.

Я знаком с Haskell, Scala, Common Lisp и немного Scheme, поэтому любые ресурсы, использующие эти языки, будут высоко оценены.

Тим Стюарт
источник
7
Вы должны проверить работу Конала Эллиота: conal.net
2
Керри-Говард изоморфизм является ключевым словом, если вы еще не знали.
Педрофурла
2
Я думал, что похожая вещь. Я пытался разработать численное моделирование точек, твердых тел и жидкости. Это ( github.com/takagi/SimulationDSL ) является одним из моих экспериментов, в которых я выразил векторную алгебру и уравнения в частных производных в Haskell DSL. Я также проверил работу Конала Эллиота.
3
Вы должны проверить LtU . Там, вероятно, есть старые добрые дискуссии, или, по крайней мере, ваш вопрос подойдет лучше, чем на SO
3
Возможно, вы захотите прочесть Сэмюэля Камина «Семантика ориентированной на реализацию симпатичных печатных комбинаторов Wadler». Он сравнивает операционные и денотационные подходы к реализации хорошо известного примера из реального мира и включает в себя пропаганду денотационного подхода.
Стивен Тетли

Ответы:

13

Денотационный дизайн ( дизайн программы основан на денотационной семантике и вытекает из нее) - моя основная методология. Несколько лет назад, когда я писал о FRP, я понял, что я делаю. См. Двухтактное функциональное реактивное программирование . Для более явного описания парадигмы и множества примеров см. Denotational design с морфизмами классов типов . Как только я осознал шаблон, я начал искать его повсюду. Где это терпит неудачу, я знаю, что у меня есть утечка абстракции. Для раннего, неофициального описания, см. Сообщение в блоге Люка Палмера Семантический дизайн» .

Я всегда заинтересован в приложениях денотационного дизайна, поэтому я хотел бы услышать о ваших исследованиях.

Conal
источник
Спасибо за большие ресурсы. Я собираюсь проверить их, прежде чем пометить вопрос как ответ.
Тим Стюарт
Спасибо за предоставление ссылок на вашу работу! Это второй раз, когда я перехожу к его изучению. К сожалению, conal.net не отвечает. Есть ли другие места, где его можно взять?
imz - Иван Захарящев
1
Ну, можно также прочитать github.com/conal/talk-2014-bayhac-denotational-design/blob/…
imz - Иван Захарящев
1
@ imz - Извините, ИванЗахарящев. Мой веб-сервер вышел из строя. Сделай резервную копию сейчас. Надеюсь, он скоро будет перенесен, и он станет более стабильным.
Конал
7

Мы применили денотационную семантику к самому языковому проектированию, утверждая, что проектирование языков, в частности, предметно-ориентированных языков, должно начинаться с определения семантики. Если вас интересуют подробности, вы, возможно, захотите взглянуть на семантику DSL Design и Semantics First! Переосмысление процесса проектирования языка .

Мартин Эрвиг
источник
Спасибо за большие ресурсы. Я собираюсь проверить их, прежде чем пометить вопрос как ответ.
Тим Стюарт