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

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

15 голосов
/ 27 декабря 2008

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

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

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

Ответы [ 4 ]

26 голосов
/ 27 декабря 2008

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

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

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

По вашему вопросу:

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

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

Здесь также есть красная сельдь: если вы посмотрите, например, на реализации монад в 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 IS-A Monad», и вы не можете проверить типовые операции, которые работают на всех экземплярах Monad.

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

0 голосов
/ 15 мая 2010

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

0 голосов
/ 11 мая 2010

Нет, в 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());
0 голосов
/ 27 декабря 2008

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

...