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

StackOverflow https://stackoverflow.com/questions/394709

Вопрос

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

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

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

Это было полезно?

Решение

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

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

Как вы, вероятно, можете судить по приведенным выше примерам, я (в основном) программист Ruby.Итак, просто в шутку, я взял один из приведенных выше примеров и повторно реализовал его на языке, который я знаю абсолютно ничего о, обычно об этом думают как о не очень мощном языке, и это, кажется, единственный язык программирования на планете, для которого я не смог найти учебное пособие по 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);
  }
));
?>

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

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

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

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

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

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

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

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

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

Другие советы

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

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

Нет, в php невозможно реализовать монады.Для этого вам нужны замыкания.Тем не менее, концепция Maybe все еще может быть полезна, когда вы моделируете сопоставление шаблонов с классами:

abstract class Maybe {
        abstract public function isJust();
        public function isNothing(){
                return !$this->isJust();
        }
}

class Just extends Maybe {
        protected $val = null;
        public function __construct($val){
                $this->val = $val;

        }
        public function isJust(){
                return true;
        }
        public function getVal(){
                return $this->val;
        }

}
class Nothing extends Maybe {
        protected $val = null;
        public function __construct(){

        }
        public function isJust(){
                return false;
        }
}

function just(){
        print "isJust";
}
function nothing(){
        print "nothing";
}
function MaybeFunc(Maybe $arg){
        if(get_class($arg) == 'Just'){
                print "Just";
        } else {
                print "Nothing";
        }
}

MaybeFunc(new Just(5));
MaybeFunc(new Nothing());
Лицензировано под: CC-BY-SA с атрибуция
Не связан с StackOverflow
scroll top