Коллеги!

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

1. Что такое система типов и зачем она на интуитивном уровне всем понятно, но я пытаюсь найти строгие формулировки для этого. Когда говорят о типах, то всегда упоминают то, что они нужны для проверки корректности программы. В попытках найти хорошую формулировку я снова обратился к излюбленному мной трактованию языка программирования, как совокупности примитивов и средств комбинации и абстракции (из SICP). Итак, язык предоставляет нам примитивы и средства комбинации этих примитивов. С этой точки зрения:

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

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

2. Но системы типов имеют и другую роль: они расширяют выразительность языка. Например, наличие системы типов позволяет производить перегрузку имен и автоматически разрешать неопределенности, с этим связанные. И вот тут я упираюсь — не могу охватить сознанием эту часть картины. В голове крутятся слова: "разрешение неопределённости", "абстракция", "семантика", "предметная область" и т.п., но воедино не складываются. Помогите преодолеть Нутром чую, что роль системы типов, как выразительного средства, можно четко сформулировать.

3. Язык программирования предоставляет средства комбинации и средства абстракции. Эти средства относятся и к типам. В теории типов они называются type constructors и предназначены для конструирования новых типов из имеющихся. Самый, наверное, распространённый пример — кортежи или записи. Часто обозначается как знак умножения, порождают новый тип, множество значений которого суть декартово произведение множеств значений типов-аргументов. Механизм абстракции позволяет нам поименовать нашу конструкцию, а кое в каких языка ещё и параметризовать её другими типами и/или значениями. Например, описание типа пары значений:

pair(T) = T * T

В связи с этим у меня возникает несколько замечаний:
3.1. Раз типы могут быть скомбинированы друг с другом, то возникает проблема проверки корректности их комбинаций и добавления выразительности. Иными словами, появляется вторая система типов, в которой значения — это типы из первой.
Примеры "из жизни": долго и мучительно обсуждаемые концепты в С++ и type classes в Haskell. Но и во второй системе типов могут быть свои комбинации и абстракции... как Вы поняли, это может продолжаться до бесконечности
Есть ли фундаментальные различия между этими системами типов?
Могут ли они быть построены на базе единого синтаксиса и семантики?

3.2. Почему в существующих ЯП (я о мэйнстриме) средства комбинации/абстракции типов так сильно отличаются от "обычных" средств комбинации и абстракции (процедур/функций, операторов и т.п.)? Ведь принципиально "обычные" и "типовые" комбинации и абстракции ни чем не отличаются. Первые описывают преобразования значений, вторые — типов, но суть у них одна: берем какие-то объекты (типы, значения), применяем к ним операторы, получаем новые объекты. Тем не менее, синтаксис описания типов и описания функций сильно отличается.

Спасибо, что прослушали весь мой поток сознания

Здравствуйте, 0x7be, Вы писали:

0>В связи с этим у меня возникает несколько замечаний:
0>3.1. Раз типы могут быть скомбинированы друг с другом, то возникает проблема проверки корректности их комбинаций и добавления выразительности. Иными словами, появляется вторая система типов, в которой значения — это типы из первой.
0>Примеры "из жизни": долго и мучительно обсуждаемые концепты в С++ и type classes в Haskell. Но и во второй системе типов могут быть свои комбинации и абстракции... как Вы поняли, это может продолжаться до бесконечности
0>Есть ли фундаментальные различия между этими системами типов?
0>Могут ли они быть построены на базе единого синтаксиса и семантики?

Да, конечно, в системах лямбда-куба и, шире, Pure Type Systems достигнут высокий уровень единообразия. Но это удобно для теоретиков и в системах управления доказательствами (proof assistants, interactive theorem provers), типа Coq. Вот пример интерактивной сессии

Coq < Check 2.
2
     : nat

Coq < Check nat.
nat
     : Set

Coq < Check Set.
Set
     : Type

Coq < Check Type.
Type
     : Type

На самом деле дальше идёт бесконечная иерархия индексированных сортов (миров)

Set : Type(i) для любого i
Type(i) : Type(j) для i < j

0>3.2. Почему в существующих ЯП (я о мэйнстриме) средства комбинации/абстракции типов так сильно отличаются от "обычных" средств комбинации и абстракции (процедур/функций, операторов и т.п.)? Ведь принципиально "обычные" и "типовые" комбинации и абстракции ни чем не отличаются. Первые описывают преобразования значений, вторые — типов, но суть у них одна: берем какие-то объекты (типы, значения), применяем к ним операторы, получаем новые объекты. Тем не менее, синтаксис описания типов и описания функций сильно отличается.

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

тип — это один из видов обобщений, причем обобщений в виде: набор требований + ряд следствий, которые из этого вытекают.
например,
тип- целое число, требование — чтобы элемент был числом и целым, следствие — может использоваться как индекс в массиве,
или
тип — коллекция с произвольным доступом, требование — последовательность поддерживает произвольный доступ, следствие — доступна операция(с оверхедом O(1)) выбрать последовательность с такого-то по такой-то индекс
и т.д.

Здравствуйте, deniok, Вы писали:

D>Да, конечно, в системах лямбда-куба и, шире, Pure Type Systems достигнут высокий уровень единообразия. Но это удобно для теоретиков и в системах управления доказательствами (proof assistants, interactive theorem provers), типа Coq.
Удобно для теоретиков, но не удобно для практиков? Почему?

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

У меня бывали такие случаи, когда надо было сделать то, что с точки зрения языка является почёсыванием за ухом левой ногой. В частности, был такой прецедент: необходимо было преобразовывать типы из вида

class X
{
  Type1 Field1;
  Type2 Field2;
  ...
}

в

class X
{
 SomeType<Type1> Field1;
 SomeType<Type2> Field1;
}

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

Здравствуйте, 0x7be, Вы писали:

0>Здравствуйте, deniok, Вы писали:

D>>Да, конечно, в системах лямбда-куба и, шире, Pure Type Systems достигнут высокий уровень единообразия. Но это удобно для теоретиков и в системах управления доказательствами (proof assistants, interactive theorem provers), типа Coq.
0>Удобно для теоретиков, но не удобно для практиков? Почему?

Ну, на практике даже в Хаскелле в системе типов над типами (кайндах) достаточно контроля арности, а более высокие уровни не нужны

Prelude> :type Just
Just :: a -> Maybe a
Prelude> :type Just 'x'
Just 'x' :: Maybe Char
Prelude> :kind Maybe
Maybe :: * -> *
Prelude> :kind Maybe Char
Maybe Char :: *
Prelude> :kind (,,,)
(,,,) :: * -> * -> * -> * -> *

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

Синтаксис всегда выбирают минимально необходимым. За дополнительные возможности мы всегда платим усложнением. Сравни, например, тип оператора композиции функций в Хаскеле и в Агде (где функциональный тип является обобщённым для поддержки зависимых типов)

-- haskell
(.) :: (b -> c) -> (a -> b) -> a -> c
(f . g) x = f (g x)

-- agda
_._ : {A : Set}{B : A -> Set}{C : (x : A) -> B x -> Set}
      (f : {x : A}(y : B x) -> C x y)
      (g : (x : A) -> B x)
      (x : A) -> C x (g x)
(f . g) x = f (g x)

Здравствуйте, 0x7be, Вы писали:

0>1. Что такое система типов и зачем она на интуитивном уровне всем понятно, но я пытаюсь найти строгие формулировки для этого.
0>

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

0>Это наиболее красивая формулировка роли системы типов, как средства доказательства корректности программ, которую я смог придумать.

Формулировка действительнок красивая. Для указанной цели подходит, а вот в общем случае, мне кажется, все не так просто. Не совсем понятно, что имеется в виду под примитивом. Вот, например:

Base a = new Derived();

Какие здесь есть примитивы?
Следует отметить, что:

1. Переменная "a" имеет тип Base.
   
2. Во время выполнения значение переменной будет типа Derived.
   
3. Во время выполнения в мейнстриме мы можем узнать тип значения переменной, а вот типы переменных теряются безвозвратно. По крайней мере я ни одного языка не знаю.

По последнему замечанию комментарий. В "обычных" случаях можно использовать "литерал" типа (в примере — Base), а вот в более сложных случаях (для generic-функций) такого нет. Пример:

let mkStrangeList x = 
  let pair = (x, x) in [x]

Я не уверен, что тип переменной pair (в данном случае 'a — обобщенный тип) можно как-либо выразить в райнтайме. Даже если взять не ml (где типы в рантайме преобразовывать нельзя), а какой-нибудь F#.

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

0>2. Но системы типов имеют и другую роль: они расширяют выразительность языка. Например, наличие системы типов позволяет производить перегрузку имен и автоматически разрешать неопределенности, с этим связанные. И вот тут я упираюсь — не могу охватить сознанием эту часть картины. В голове крутятся слова: "разрешение неопределённости", "абстракция", "семантика", "предметная область" и т.п., но воедино не складываются. Помогите преодолеть Нутром чую, что роль системы типов, как выразительного средства, можно четко сформулировать.

Ваше исходное определение здесь тоже хорошо подходит. А выразительность программ здесь повышает не столько наличие системы типов сколько возможность "именовать" сущности языка программирования (в том числе — типы и какие-либо связи между ними). Что же касается перегрузки ("разрешения неоднозначностей") — это спорный вопрос. Некоторые языки вообще запрещают неоднозначность. Другие разрешают неопределенности на базе compile-time типов (перегрузка в mainstream). Третьи вообще выполняют разрешение неоднозначностей в runtime (мультиметоды в Lisp, виртуальные методы в mainstream). И "повышение выразительности" перегрузкой методов вопрос вообще спорный, особенно когда правила разрешения таких случаев занимают несколько страниц текста (та же java).

0>3.2. Почему в существующих ЯП (я о мэйнстриме) средства комбинации/абстракции типов так сильно отличаются от "обычных" средств комбинации и абстракции (процедур/функций, операторов и т.п.)? Ведь принципиально "обычные" и "типовые" комбинации и абстракции ни чем не отличаются. Первые описывают преобразования значений, вторые — типов, но суть у них одна: берем какие-то объекты (типы, значения), применяем к ним операторы, получаем новые объекты. Тем не менее, синтаксис описания типов и описания функций сильно отличается.

Здесь фокус в том, что в мейнстриме значения (включая процедуры и функции) и типы имеют разную природу.

1. Во всем mainstream тип не является first-class object. Его нельзя сохранить в переменную, вернуть откуда-нибудь и т.п. То, что можно делать в mainstream'е, работает не с теми типами, с которыми работает компилятор (см. ответ на первый пункт). Да, можно получить через рефлексию информацию о типе значения, но очень сложно создать даже новый runtime-тип. И это будет именно runtime-тип.
   
2. Все комбинаторы работают со значениями времены выполнения. Сравните удобство комбинирования функций в pascal'е и том же F#/ocaml. На динамических языках можно и еще более сложные "комбинаторы" и "трансформеры" записывать, но они, опять же, будут работать с типами времены "выполнения" а не компиляции. Пример таких трансформеров — "оборачивание" функции (с "произвольным" числом аргументов) в обработку исключений.
   
3. Для работы с "конвертерами" типов гораздо больше подходит "структурная" типизация, чем номинативная. Потому что если мы допускаем "комбинацию" типов с помощью определяемого комбинатора, хотелось бы, чтобы "одинаково записываемые" типы были одним и тем же типом в разных модулях. Т.е. applyTypeTransformation(SomeType) был бы одним и тем же типом в различных местах.
   
4. Все вычисления "типов" компилятор делает во время компиляции. Так что даже если была бы возможность создавать типы во время выполнения, не понятно, что это дало бы. Да, создавать значения новых "типов" — нужно. А вот сами типы — вопрос спорный. Например, создали мы var myTyple = mkTyple([int, String]), а что с ним делать дальше?

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

Второй — перенос всех типов до уровня "first-class objects" и структурная типизация. Детально не продумывал, могут быть проблемы. В этом случае "аннотация типа" всего лишь является дополнительной "проверкой" для значения этого типа. Что-то вроде:

type myVariant = variant([('VariantA', int), ('VariantB', SomeType)];
let f x : myVariant = ... "генерирует" два значения:
let safe f x = ... (здесь предполагается, что x уже точно имеет тип myVariant)
let unsafe f x = matchType(x, myVariant); safe f x

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

Все "классические" типы из мейнстрима при этом можно построить во время компиляции. Т.е. все значения аргументов для "type-constructor method" будут константами времени компиляции (в основном это будут другие типы). Какие-то вещи можно будет построить в рантайме и валидировать их. Здесь много проблем с определением "константности" типов и функций во время компиляции. Ну и вопросы с тем, не понравится ли пользователям делать "динамические преобразования" слишком много, так, что вся работа с типами будет в рантайме . Либо можно попробовать ограничить возможности для работы с типами (что-то вроде шаблонов в D, они, кстати, могут иметь более продвинутый доступ к типам), тогда можно будет полностью построить все "необходимые" типы на этапе компиляции.

Динамика здесь хороша еще тем, что "достаточно прозрачно" можно создавать объекты "новых" типов во время выполнения.

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

Здравствуйте, 0x7be, Вы писали:

0>2. Но системы типов имеют и другую роль: они расширяют выразительность языка. Например, наличие системы типов позволяет производить перегрузку имен и автоматически разрешать неопределенности, с этим связанные. И вот тут я упираюсь — <...> Нутром чую, что роль системы типов, как выразительного средства, можно четко сформулировать.

Они ничего не расширяют. Сначала мы ограничиваем применение функции

void func(int a);

Только к переменным типа int (в си ещё преобразование типов допускается).
А потом "расширяем" язык разрешая делать

void func(const MyClass& c);

Но без 1го шага можно было бы просто использовать функцию func, которая принимает 1 аргумент любого типа.
То, что вызовется нужная функция func не более чем синтаксический сахар.