Вопрос по алгебраическим типам

Представление типов множествами это такая операция, к которой нужно подходить аккуратно (правда, я не уверен что могу объяснить почему). Ну да ладно, допустим, что тип == множество значений.

Теперь просто о множествах, безотносительно того, считаем ли мы их типами. Пусть есть совокупность множеств, проиндексированных множеством I: { A_i }_{i \in I}. Дизъюнктное объединение строится так: каждый элемент множества A_i — a \in A_i — превращается в пару (a, i) (или (i, a), неважно) и потом все эти пары сливаются в одно множество, которое мы и называем дизъюнктным объединением.

Это простейшая конструкция, которая реализует копроизведение в категории множеств.

Где можно увидеть пример такого объединения представленный в коде какого-нибудь ЯП?

В той же статье, не?

struct Tree {
    union {
        int value;
        struct {
            struct Tree *left;
            struct Tree *right;
        } branches;
    } data;
    enum { LEAF, NODE } selector;
};

Короче, variant это. А конструкторы это функции, которые заполняют поля данных.

{-|
  A value of type 'Dynamic' is an object encapsulated together with its type.

  A 'Dynamic' may only represent a monomorphic value; an attempt to
  create a value of type 'Dynamic' from a polymorphically-typed
  expression will result in an ambiguity error (see 'toDyn').

  'Show'ing a value of type 'Dynamic' returns a pretty-printed representation
  of the object\'s type; useful for debugging.
-}
data Dynamic = Dynamic TypeRep Any

пожалуйста.

P.S. я наврал про ограничение, мне казалось там Fingerprint а не TypeRep лежит.

вот это I: { A_i }_{i \in I} предполагает просмотр в человеческом виде или нет? если препдолагает, то что поставить чтобы увидеть?

Не предполагает, т.к. для того, чтобы это отображалось в TeX так, как задумывалось, нужно записать как \{ A_i \}_{i \in I}

В Rust

enum MyType {
   Foo(SomeType1),
   Bar(SomeType2),
}

спс

Отлично. И где профит с этого?

не шарю в плюсах и паскалях, но variant разве может содержать разные, скажем, int?

  Int     Int
    \     /
     \   /
    [variant]

Короче, variant это

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

Не знаю насчет variant, но в плюсах можно изобразить sum type, очень похожий на настоящий.

это-то понятно :]

Показали, что в категории множеств есть копроизведения, предъявив явную конструкцию этого копроизведения. Ну. Нестрого. Мне лень строго. И вообще.

Динамически типизированные языки это узкое подмножество статически типизированных. В статически типизированных языках ты можешь наделать себе каких угодно sum types.

А вот в динамически типизированном языке у тебя есть только один тип и он является sum type.

Зашибись (в смысле «здОрово») И профит в чём?

в динамически типизированном языке у тебя есть только один тип

Почему? Или это Ваше личное предположение?

в динамически типизированном языке у тебя есть только один тип

Почему?

А ты больше насчитал?

Да, как правило даже примитивных типов порядка десяти

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

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

Так что всё, что у тебя есть — это sum type из этих «примитивных типов» и тебе доступен только этот sum type, а «примитивные типы» явно недоступны.

В динамически-типизированных языках нет вот этого сахара с конструкторами и паттерн матчингом, да и явных ограничений на типы тоже нет (а тут они явно перечислены). Ну и без точных определений не было бы связи с математикой и не было бы аппарата для рассуждений. Просто реализуется оно по сути как variant (какие-то детали могут отличаться).

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

Впрочем, тот факт, что написанием таких инструментов особо никто не заморачивается, говорит о том, что это никому не нужно, в массе.

Наличие статически типизированных языков говорит об обратном, а отсутствие «таких инструментов» (для динамических языков) может говорить только о том, что оно не нужно любителям динамики. Впрочем, и последнее не похоже на правду: ведь есть всякие TypeScript, да и в ряде динамических языков имеется возможность типы указывать.

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

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

kek

но формально тогда variant это не sum type. А ввот с тегами это уже ближе к требуемому.

Так это же не встроенный тип, реализовать можно по-всякому. Просто когда типы не повторяются, то они же и служат тегами.

странного утверждения анонимуса о якобы отсутствии типов в динамически-типизированных языках

Это не странное утверждение, это элементарный факт. https://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static...

sum type, очень похожий на настоящий

Можно ссылку?

P.S. Нашёл, но на самом деле нет: Mission critical C++ (комментарий) . Там ссылка сдохла.

http://pastebin.com/bvBkMhkp

реализует копроизведение

Хорошее слово.
Копроизведение - это то, что реализовал (в этот раз) модератор Klymedy.

В Вики, даже в русскоязычной, по АТД есть отличная статья. В англоязычной отличные, простым языком написанные, статьи про юнионы, тегирование, сравнение по разным языкам и периодам, доходчивые объяснения. Теории завались, чего тут спорить. Любое тегированное объединение и есть АТД, состоявшееся еще в 60-х в АЛГОЛЕ.

Ну как ни странно он прав. Динамика требует дисциплины и более высокой квалификации, иначе код очень-очень быстро переходит в неподдерживаемое состояние.