Должен ли язык, который реализует Monads, статически типизирован?

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

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

Ответы

Ответ 1

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

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

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

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

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

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

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

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

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

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

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

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

Ответ 2

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

Ответ 3

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

Ответ 4

Нет, в 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());