Недавно я глубоко заинтересовался Хаскеллом.
Пытаясь изучить новые концепции (например, ключевое слово forall и монаду ST ) и систему типов Хаскеля в целом, я постоянно сталкиваюсь с понятиями из теории категорий и лямбда-исчисления . Итак, мне интересно:
Какие другие разделы математики важны для глубокого понимания системы типов Хаскелла?
Могу ли я отказаться от тщательного изучения математики и сосредоточиться на определенных подходящих понятиях? (например, квантификаторы в лямбда-исчислении.) Если да, то какие понятия важны?
Я надеюсь в скором времени подобрать типы и языки программирования , однако, пожалуйста, предложите любые альтернативные ресурсы для чтения, которые вы считаете подходящими.
STмонаде. Трудно написать код, который будет компилироваться, когда я не понимаю всех соответствующих сигнатур типов, поэтому я чувствовал, что было бы разумно улучшить мое понимание системы типов.Ответы:
Нет, вам не нужно поднимать книгу по теории категорий, чтобы понять Haskell.
Я использую Haskell в течение нескольких лет, и из любопытства подобрал некоторую теорию категорий, в этом действительно нет необходимости. С одной стороны, здорово видеть, как все эти абстракции вписываются в «общую картину», но я не сказал «О, черт возьми, мне просто нужно сделать этого профессора из
Maybeкатегории в[]s, а затем я могу сохранить принцесса!».Теперь, в зависимости от того, что вы делаете с теорией типов Хаскелла, стоит на пороге.
Если вы только изучаете haskell , не пытайтесь понять каждый нюанс системы типов . Пожалуйста, не надо, это все равно, что пытаться сначала изучить метапрограммирование на C ++. Необычные типы являются отличными инструментами, но хорошее понимание функционального программирования превосходит понимание непредсказуемого полиморфизма.
Теперь, скажем, через год или два из Haskell вы хотите понять каждую тонкую часть работы системы типов Haskell, тогда да, некоторая теория типов может оказаться полезной.
Это поможет вам понять некоторую логику, лежащую в основе того, как все работает, плюс, честно говоря, это действительно крутая отрасль компьютерных наук IMO, на которую стоит обратить внимание. Вы можете выбрать те части, которые вас интересуют, и при этом узнать приличную сумму.
Для Haskell, рассматривая STLC, системы типа HM (System F) и, возможно, лямбда-куб (Haskell - это System Fw iirc) и изорекурсивные типы. Типы и языки программирования - отличный ресурс для начала и охватывает все это и многое другое.
Если вы действительно хотите выпить классную помощь и обнаружите, что вы - начинающий теоретик, идите тыкать в Agda или Coq. Они имеют «зависимые типы», на один шаг дальше в лямбда-кубе, чем Haskell. Зависимые типы позволяют типам зависеть от условий. Это означает, что типы достаточно сильны, чтобы фактически доказать теоремы. Для любопытных, поиск в Google "изоморфизма Карри Ховарда" должен принести некоторые интересные результаты.
источник