Должен ли язык, реализующий монады, быть статически типизированным?

Я изучаю функциональный стиль программирования. В Не бойтесь монад Брайан Бекман блестяще рассказал о Монаде. Он упомянул, что Monad — это композиция функций для решения проблемы сложности.

Монада включает в себя функцию unit, которая переводит тип T в усиленный тип M(T); и функция Bind, которая при заданной функции от T до M(U) преобразует тип M(T) в другой тип M(U). (U может быть T, но не обязательно).

В моем понимании язык, реализующий монаду, должен проверяться статически. В противном случае ошибки типа не могут быть обнаружены во время компиляции, а «сложность» не контролируется. Правильно ли я понимаю?


person Morgan Cheng    schedule 27.12.2008    source источник


Ответы (4)


Существует множество реализаций монад в динамически типизированных языках:

В общем, Тезис Черча-Тьюринга говорит нам, что все, что можно сделать на одном языке, можно сделать и на любом другом языке.

Как вы, наверное, поняли из приведенных выше примеров, я (в основном) программист на Ruby. Итак, просто в шутку я взял один из приведенных выше примеров и повторно реализовал его на языке, о котором я абсолютно ничего не знаю, который обычно считается не очень мощным языком, и который кажется, это единственный язык программирования на планете, для которого я не смог найти туториал по монадам. Позвольте представить вам… Identity Monad в PHP:

<?php
class Identity {
  protected $val;
  public function __construct($val) { $this->val = $val; }
  public static function m_return($a) { return new Identity($a); }
  public static function m_bind($id_a, $f) { return $f($id_a->val); }
}

var_dump(Identity::m_bind(
  Identity::m_return(1), function ($x) {
    return Identity::m_return($x+1);
  }
));
?>

Никаких статических типов, никаких дженериков, никаких замыканий.

Теперь, если вы действительно хотите статически проверять монады, вам нужна статическая система типов. Но это более или менее тавтология: если вы хотите статически проверять типы, вам нужна статическая проверка типов. Дух.

Что касается вашего вопроса:

В моем понимании язык, реализующий монаду, должен проверяться статически. В противном случае ошибки типов не могут быть обнаружены во время компиляции, а сложность не контролируется. Правильно ли я понимаю?

Вы правы, но это не имеет ничего общего с монадами. Это касается проверки статического типа в целом и одинаково хорошо применима к массивам, спискам или даже к простым скучным целым числам.

Здесь также есть отвлекающий маневр: если вы посмотрите, например, на реализации монад на C#, Java или C, они намного длиннее и намного сложнее, чем, скажем, пример PHP выше. В частности, везде есть тонны типов, так что это, безусловно, выглядит впечатляюще. Но горькая правда такова: системы типов C#, Java и C на самом деле недостаточно мощны, чтобы выразить тип Monad. В частности, Monad является полиморфным типом ранга 2, но C# и Java поддерживают только полиморфизм ранга 1 (они называют его дженериками, но это одно и то же), а C не поддерживает даже это.

Таким образом, монады на самом деле не подвергаются статической проверке типов в C#, Java и C. не может выразить тип в C#.) Все, что делает система статического типа, это делает реализацию намного сложнее, фактически не помогая. Требуется гораздо более сложная система типов, такая как Haskell, чтобы обеспечить реальную безопасность типов для монад.

Примечание: то, что я написал выше только, относится к самому универсальному типу monad, как указывает @Porges. Конечно, вы можете указать тип любой конкретной монады, такой как List или Maybe, но вы не можете выразить тип самой Monad. А это значит, что вы не можете проверить тип того факта, что List ЯВЛЯЕТСЯ Monad, и вы не можете проверить типовые операции, которые работают со всеми экземплярами Monad.

(Обратите внимание, что проверка того, что Monad также подчиняется законам монады в дополнение к соответствию монадному типу, вероятно, слишком сложна даже для системы типов Haskell. Вам, вероятно, понадобятся зависимые типы. и, возможно, даже полноценный автоматический доказатель теорем для этого.)

person Jörg W Mittag    schedule 27.12.2008
comment
Существует также очень хорошая библиотека Clojure clojure.contrib.monads, дополненная рядом отличных руководств (ссылки на некоторые из них включены в исходный код библиотеки). - person Michał Marczyk; 19.12.2009
comment
Я думаю, что последний абзац и немного вводят в заблуждение. Это интерфейс Monad<T>, который не реализуем на Java/C# (и, следовательно, тавтологически не проверяется тип!). С другой стороны, для конкретной монады наверняка возможна статическая проверка типов. - person porges; 12.05.2010

Это, конечно, не тот случай, когда язык, реализующий монады, должен быть статически типизированным, как указано в заголовке вашего вопроса. Это может быть хорошей идеей по причинам, которые вы изложили, но ошибки, которые не могут быть обнаружены во время компиляции, никогда никого не останавливали. Вы только посмотрите, сколько людей пишут на PHP.

person chaos    schedule 27.12.2008
comment
Я не уверен, но любой шаблон в PHP является монадой? - person Morgan Cheng; 27.12.2008

Вам нужны замыкания для монады State. Я посмотрел, в PHP есть замыкания с 5.3. Так что это уже не будет проблемой.

person Edgar Klerks    schedule 15.05.2010
comment
PHP 5.3 имеет анонимную функцию, которая не совсем закрыта. - person Morgan Cheng; 15.05.2010
comment
Полная мощность замыкания на самом деле не нужна; все, что нам нужно сделать, это объединить и преобразовать функции; анонимные функции подойдут. - person Jonathan Sterling; 19.10.2010

person    schedule
comment
Я сомневаюсь, что. Во-первых, в PHP есть замыкания. А во-вторых, я не понимаю, зачем вам нужны замыкания для реализации монад. См. мой ответ для реализации Identity Monad в PHP, которая не использует замыкания. В конце концов, PHP — это полный по Тьюрингу язык, и все, что вы можете сделать на одном полном по Тьюрингу языке, можно сделать и на любом другом полном по Тьюрингу языке. Итак, если вы можете реализовать монады на Haskell, то вы можете сделать это и на PHP. - person Jörg W Mittag; 12.05.2010