Использование системы «сильного» типа в реальном мире, скажем, для крупномасштабных веб-приложений?

Я знаю, что это очень широкий, неоднозначный и, возможно, философский вопрос. В той степени, что самое важное ключевое слово в вопросе - «сильная» система типов - само по себе плохо определено . Итак, позвольте мне попытаться объяснить, что я имею в виду.

Общий контекст вопроса

Мы создавали очень масштабное веб-приложение на Ruby on Rails и в целом были довольны нашим стеком. Когда мы захотим, мы сможем доставить материал очень быстро - то, что подходит для 90% «бизнес-кейса», не беспокоясь о 10% крайних случаях. С другой стороны, с помощью обзоров кода и охвата тестами мы можем быть медленными и обдуманными и обеспечивать охват всех баз - опять же, только в ситуациях, которые заслуживают такого тщательного изучения и безопасности.

Однако, по мере роста команды, я начал чувствовать себя некомфортно из-за отсутствия «защитной сетки», запеченной прямо в нашем стеке.

Недавно мы начали делать некоторые разработки для Android на Java. И мне (приятно) напомнили о безопасности, обеспечиваемой скомпилированным / статическим / строго типизированным языком.

• Неправильно написанные переменные, неправильные типы данных, неправильные вызовы функций и множество простых ошибок выявляются самой IDE. Все потому, что IDE может подключиться к компилятору и проверить определенные аспекты "правильности" программы.
• Нужно изменить сигнатуру функции? Легко. Компилятор + IDE может помочь вам определить ВСЕ сайты вызовов.
• Необходимо убедиться, что определенные исключения всегда обрабатываются? Проверены исключения для вашего спасения.

Теперь, когда эти функции безопасности имеют свои преимущества, я хорошо знаю и их недостатки. Тем более, что в мире «шаблонной тяжелой» Java. Поэтому вместо Java я начал изучать множество современных «строго типизированных» языков, над которыми люди начали работать в эти дни. Например: Scala, Rust, Haskell и т. Д. Меня больше всего интересует мощь их систем типов и статические проверки / проверки во время компиляции.

Теперь вопрос

Как использовать эти мощные системы типов и статические функции / функции времени компиляции в больших приложениях?

Например, как бы я вышел за рамки стандартного вида «привет мира», посвященного этим мощным функциям? Тот, который использует богатую систему типов для моделирования проблемы бизнес-домена? Система типов помогает или мешает, когда вы находитесь в зоне 30000 LOC +? Что происходит с сетью безопасности, предоставляемой этими системами типов (и проверками времени компиляции), когда ваша система взаимодействует со слабо типизированным внешним миром, например. через JSON или XML API, различные хранилища данных, пользовательский ввод и т. д.

Я дам короткий ответ из-за нехватки времени на данный момент, но в настоящее время я работаю над двумя крупными проектами (> 100 000 LOC в Haskell) - flowbox.io и luna-lang.org, Мы используем Haskell для всех частей, включая бэкэнд, компилятор нашего языка программирования и даже графический интерфейс на основе webGL. Я должен признать, что система сильного типа и механизм, подобный «зависимому типу», могут направлять вас и избавлять вас от бремени и хлопот, известных на других языках. Мы очень широко используем типы, и все, что можно было проверить во время компиляции, сделано так. Фактически, за последние 3 года разработки мы никогда не сталкивались с ошибками во время выполнения или переполнением стека (и это действительно невероятно). Единственными ошибками являются очевидные логические ошибки, допущенные программистами. Многие люди говорят, что если что-то компилируется в Haskell, это просто работает, и вы должны быть уверены, что это не произойдет.

Отвечая на первую часть вопроса: вы можете узнать об этих мощных функциях системы типов, прочитав несколько замечательных блогов, таких как:

• Блог Бартоша Милевского
• Эдвард Кметт один
• или Габриэль Гонзалес один

На самом деле, есть много других хороших блогов (например, планета Хаскелл ). В любом случае, лучший способ по-настоящему понять продвинутые системы типов - это разработать полезную библиотеку с открытым исходным кодом. Мы (в Flowbox & New Byte Order) выпускаем много библиотек (вы можете найти их в Hackage), поэтому, если у вас нет идеи, что разрабатывать, вы всегда можете подключиться к нашим проектам - просто напишите мне, когда вы хочу (почта доступна на luna-lang.org ).

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

Поэтому я предпочитаю определение:

• Слабо типизированные системы используют типы, чтобы помешать вам делать определенные вещи (например, ошибки)
• Строго типизированные системы используют типы, чтобы сделать что-то для вас

Что я имею в виду, делая вещи для вас? Что ж, давайте рассмотрим написание API для преобразования изображений в инфраструктуре Servant (в Haskell, но вам не нужно знать, что нужно, чтобы следовать, вы увидите ...)

{-# LANGUAGE
    TypeOperators,
    DataKinds
    #-}

import Codec.Picture
import Data.Proxy
import Network.Wai.Handler.Warp (run)
import Servant
import Servant.JuicyPixels

main :: IO ()
main = run 8001 conversion

Это говорит о том, что нам нужны некоторые модули, в том числе пакет Servant и плагин JuicyPixels, в Servant, и что основной точкой входа в программу является запуск функции «преобразования» на порту 8001 в качестве сервера с использованием бэкэнда Warp. Не обращайте внимания на язык немного.

conversion :: Application
conversion = serve (Proxy :: Proxy ConversionApi) handler

Это говорит о том, что функция преобразования является сервером, где API должен соответствовать типу «ConversionApi», а запросы обрабатываются функцией handler

type ConversionApi
     = ReqBody '[BMP, GIF, JPEG 50, PNG, TIFF, RADIANCE] DynamicImage
    :> Post '[BMP, GIF, JPEG 50, PNG, TIFF, RADIANCE] DynamicImage

Это указывает ConvesionApiтип. Он говорит, что мы должны принять входящие типы контента, указанные в списке '[BMP, GIF, JPEG 50, PNG, TIFF, RADIANCE], и обработать их как DynamicImage, и что мы должны вернуть DynamicImage, преобразованный в тот же диапазон контента типы. Не беспокойтесь о том, что:> означает, просто покажите это счастливой магией.

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

• Вы не возвращаете неправильный исходящий тип контента
• Вы не анализируете входящий запрос как неправильный тип контента
• Если бы наш сервер был более сложным, это помешало бы нам создавать искаженные URI, но на самом деле мы не возвращаем никаких HTML-страниц, содержащих ссылки (а тип гарантирует, что мы не можем!)
• Действительно амбициозная система слабой типизации может даже проверить, чтобы убедиться, что мы исчерпывающе обрабатываем все входящие и исходящие типы контента, позволяя типу также действовать как документ спецификации, а не просто как ограничение.

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

handler = return

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

Итак, как вы научитесь делать это в масштабах основных приложений? Ну, это не сильно отличается от использования их в небольших приложениях. Типы, которые являются абсолютными, не заботятся о том, сколько кода написано относительно них.

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

Таким образом, это в основном просто практика моделирования вещей с типами. Два основных способа моделирования вещей (или построения вещей в целом) - снизу вверх и сверху вниз. Нисходящий процесс начинается с наивысшего уровня операций, и при построении модели у вас есть детали, на которые вы откладываете моделирование на потом. Моделирование снизу вверх означает, что вы начинаете с базовых операций, точно так же, как вы начинаете с базовых функций, затем строите все большие и большие модели, пока вы полностью не захватите работу проекта. Внизу более конкретный и, вероятно, быстрее построить, но сверху вниз может лучше информировать ваши модели нижнего уровня о том, как они должны вести себя на самом деле.

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

Насколько я могу предложить, типы могут быть разделены следующим образом:

• Очень слабый тип, такие вещи, как JavaScript, где определено [] + {}
• Слабо набирается как Python, где вы не можете сделать [] + {}, но это не проверяется, пока вы не попробуете
• Слабая типизация, например C или Java, где вы не можете сделать [] + {}, но это проверяется во время компиляции, однако у вас нет более продвинутых функций типа
• Преодолевая границу между слабо и строго типизированным, таким как метапрограммирование шаблонов C ++, и более простым кодом на Haskell, где типы обеспечивают только свойства.
• Полностью в строго типизированных, как более сложные программы на Haskell, где типы делают вещи, как показано выше
• Очень строго типизированный, такой как Agda или Idris, где типы и значения взаимодействуют и могут ограничивать друг друга. Это так же сильно, как системы типов, и программирование в них такое же, как написание математических доказательств того, что делает ваша программа. Примечание: кодирование в Agda - это не буквальное написание математических доказательств, типы - это математические теории, а функции с этими типами являются конструктивными примерами, доказывающими эти теории.

Как правило, чем дальше вы идете по этому списку, тем больше типов могут сделать для вас, но на самом деле вы забираетесь в стратосферу, и воздух становится немного тоньше - экосистема пакета намного меньше, и вы ' Я должен буду написать больше вещей, а не найти соответствующую библиотеку. Барьер для входа также возрастает по мере того, как вы спускаетесь, поскольку вы должны понимать систему типов, достаточную для написания крупномасштабных программ.

Я только начал работать над основной командой большой платформы, написанной на Scala. Вы можете посмотреть на успешные приложения с открытым исходным кодом, такие как Scalatra, Play или Slick, чтобы увидеть, как они справляются с некоторыми из ваших более подробных вопросов о взаимодействии с динамическими форматами данных.

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

Конечно, не все принципы проектирования могут быть применены в системе типов, но чем сильнее ваша система типов, тем больше принципов проектирования вы можете применять в компиляторе.

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

Строгая типизация также помогает различать такие вещи, как необработанный и дезинфицированный ввод, что может помочь в обеспечении безопасности.

Строгая типизация также помогает вашим тестам быть более сфокусированными на вашем реальном поведении , вместо того, чтобы требовать кучу тестов, которые просто тестируют ваши типы. Это делает тестирование намного более приятным, более сфокусированным и, следовательно, более эффективным.

Основным недостатком является незнание языка и языковой парадигмы, и это со временем можно исправить. Кроме того, мы нашли, что оно того стоит.

Хотя это и не прямой ответ (так как я еще не работал над +30.000 LOC-кодами в haskell :( ..), я умоляю вас проверить https://www.fpcomplete.com/business/resources/case-studies / который включает в себя множество примеров использования haskell в реальных промышленных условиях.

Еще одна хорошая статья - IMVU, в которой описывается их опыт перехода на haskell - http://engineering.imvu.com/2014/03/24/what-its-like-to-use-haskell/ .

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

Я дам пару ссылок на ресурсы, которые я рекомендую, поскольку вы задаете довольно много вопросов одновременно:

• Небольшая серия по общим оптимизациям, в haskell
• Мышление в типах
• Так как вы находитесь в мире веб-разработчиков, я предлагаю проверить Yesod , который является одной из самых удивительных веб-фреймворков в haskell (имеет безопасные маршруты и многое другое).

В качестве заключительного замечания, отношение к внешнему миру делается несколькими способами. Существуют библиотеки, которые обеспечивают безопасность типов, например, Aeson для JSON, Esqueleto для SQL и многие другие.

Что я видел:

Я работал над несколькими крупными веб-приложениями на Ruby (Rails), одним большим веб-приложением на Haskell и несколькими более мелкими. Имея этот опыт, я должен сказать, что жизнь в приложениях на Haskell намного проще, чем в Rails, в таких аспектах, как обслуживание и низкая скорость обучения. Я придерживаюсь мнения, что эти преимущества обусловлены как системой типов Haskell, так и стилем функционального программирования. Однако, в отличие от многих, я считаю, что «статическая» часть системы типов - это просто огромное удобство в том, что при использовании динамических контрактов все еще есть преимущество.

Во что я верю

Существует замечательный пакет, называемый Contracts Ruby, который предоставляет некоторые основные функции, которые, как мне кажется, помогают проектам на Haskell улучшить характеристики обслуживания. Контракты Ruby выполняет свои проверки во время выполнения, поэтому лучше всего в сочетании с высокой степенью сходимости теста, но он все же предоставляет ту же встроенную документацию и выражение намерения и значения, что и использование аннотаций типов в таких языках, как Haskell.

Ответ на вопрос

Чтобы ответить на поставленные выше вопросы, есть много мест, где можно познакомиться с Haskell и другими языками с продвинутыми системами типов. Тем не менее, и, честно говоря, хотя эти источники документирования сами по себе превосходны, все они кажутся немного подавляющими по сравнению с множеством документации и практическими советами, которые можно найти в Ruby, Python, Java и других подобных языках. В любом случае, Real World Haskell стареет, но все еще является хорошим ресурсом.

Теория категорий

Если вы выберете Haskell, вы столкнетесь с большим количеством литературы, в которой обсуждается теория категорий. ИМХО теория категорий полезна, но не обязательна. Учитывая распространенность в сообществе Haskell, легко сопоставить плюсы и минусы типов с чувствами по поводу практичности теории категорий. Полезно помнить, что это две разные вещи, то есть реализации, управляемые теорией категорий, могут выполняться как в динамически типизированных языках, так и в статических (по модулю преимуществ, предоставляемых системой типов). Продвинутые системы типов вообще не связаны с теорией категорий, а теория категорий не связана с системами типов.

Подробнее о типах

По мере того, как вы узнаете больше о программировании с типами и их приемах (что происходит довольно быстро, потому что это весело), ​​вы захотите больше выразить с помощью системы типов. В этом случае я обращаюсь к некоторым из следующих ресурсов и присоединяюсь ко мне, чтобы поставщики инструментов знали, что мы хотим, чтобы инструменты промышленного качества, с этими функциями, были упакованы только в нечто, демонстрирующее простой в использовании интерфейс (например, Contracts Ruby):

• Введение в программирование в ATS

• Типы уточнения LiquidHaskell через SMT и предикатную абстракцию

• Разработка на основе типов с помощью Idris

Во-первых, я чувствую, что существует путаница в ответах между слабо типизированным и строго типизированным и статическим и динамически типизированным. Ссылка на предоставленный ОП четко разграничивает:

Сильная система типов - это система типов, которая имеет ограничение времени компиляции или функцию времени выполнения, которая вам кажется привлекательной.

Слабая система типов - это система типов, в которой отсутствует это ограничение или особенность.

Например, C, C ++ и Java имеют статическую типизацию, поскольку переменные вводятся во время компиляции. Тем не менее, C и C ++ можно считать слабо типизированными, поскольку язык позволяет обходить ограничения с помощью void *указателей и приведений. Больше на эту тему.

При таком различии строгая типизация может быть только лучше. Чем раньше провал, тем лучше.

Однако при написании больших программ я не думаю, что система типов играет важную роль. Ядро Linux - это десять миллионов LOC, написанных на C и ассемблере, и считается очень стабильной программой, это далеко от моих 200 строк Java, которые, вероятно, полны дыр в безопасности. Точно так же, хотя динамически типизированные «языки сценариев» имеют плохую репутацию, когда речь идет о написании больших программ, иногда есть доказательства того, что они незаслуженные (например, Python Django, более 70 тыс. LOC)

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

Где можно прочитать о том, как использовать эти мощные системы типов и статические функции / функции времени компиляции в более крупных приложениях?

из предыдущего ответа https://www.fpcomplete.com/business/resources/case-studies/

Как можно выйти за рамки стандартного вида «привет мира», знакомящего с этими мощными функциями?

это действительно как любой другой язык для наращивания силы

Как можно использовать систему с богатыми типами для моделирования проблемы бизнес-домена?

Используя абстрактные типы данных или, в более общем смысле, полиморфизм

Система типов помогает или мешает, когда вы находитесь в зоне 30000 LOC +?

Это помогает полностью. система типов помогает вам написать код, поскольку он сообщает вам форму результата, который вы хотите получить. На самом деле Агда написать код для вас.

PS: не делайте ошибку, имея систему типов и пишите типы самостоятельно, что идиотично: компьютер может сделать это за вас.

Что происходит с сетью безопасности, предоставляемой этими системами типов (и проверками времени компиляции), когда ваша система взаимодействует со слабо типизированным внешним миром, например. через JSON или XML API, различные хранилища данных, пользовательский ввод и т. д.

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

Если вы действительно хотите знать о типах и абстракции, лучше всего познакомиться с понятиями о типах, абстракции данных и полиморфизме.

Это бумага, а не тематическое исследование с красивыми картинками, но это поучительно

Как программист .net, который много работает с веб-приложениями, я вижу как типизированный C #, так и нетипизированный Javascript.

Я не уверен, что видел литературу по вопросам, которые вы задаете. С печатным языком вы принимаете все эти вещи как должное. С нетипизированным вы видите определение типов как ненужные накладные расходы.

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

Если вы хотите написать очень короткую программу, возможно, определив функцию в несколько строк для работы с более крупным приложением, то у вас просто нет места для объявления классов. Конечно, это нишевые нетипизированные языки, такие как JS?