История изменений

Мне кажется, несмотря на то что вроде как жидкие типы выглядят проще, эта простота обманчива.

Похоже, внутри жидких типов зависимые типы. Статья, цитата:

We present Logically Qualified Data Types, abbreviated to LiquidTypes, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid types allow programmers to reap many of the benefits of dependent types, namely static verification of critical properties and the elimination of expensive run-time checks, without the heavy price of manual annotation.

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

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

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

1) кажется, что жидкие типы должны быть менее выразительны (иначе за счёт чего достигается простата и возможность использовать Хиндли-Милнера для вывода?)

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

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

Мне кажется, несмотря на то что вроде как жидкие типы выглядят проще, эта простота обманчива.

Внутри жидких типов зависимые типы. Статья, цитата:

We present Logically Qualified Data Types, abbreviated to LiquidTypes, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid types allow programmers to reap many of the benefits of dependent types, namely static verification of critical properties and the elimination of expensive run-time checks, without the heavy price of manual annotation.

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

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

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

1) кажется, что жидкие типы должны быть менее выразительны (иначе за счёт чего достигается простата и возможность использовать Хиндли-Милнера для вывода?)

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

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

Мне кажется, несмотря на то что вроде как жидкие типы выглядят проще, эта простота обманчива.

Внутри жидких типов зависимые типы. Статья, цитата:

We present Logically Qualified Data Types, abbreviated to LiquidTypes, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid types allow programmers to reap many of the benefits of dependent types, namely static verification of critical properties and the elimination of expensive run-time checks, without the heavy price of manual annotation.

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

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

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

1) кажется, что жидкие типы должны быть менее выразительны (иначе за счёт чего достигается простата и возможность использовать Хиндли-Милнера для вывода?)

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

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

Мне кажется, несмотря на то что вроде как жидкие типы выглядят проще, эта простота обманчива.

Внутри жидких типов зависимые типы. [Статья](http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf)), цитата:

We present Logically Qualified Data Types, abbreviated to LiquidTypes, a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. Liquid types allow programmers to reap many of the benefits of dependent types, namely static verification of critical properties and the elimination of expensive run-time checks, without the heavy price of manual annotation.

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

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

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

1) кажется, что жидкие типы должны быть менее выразительны (иначе за счёт чего достигается простата и возможность использовать Хиндли-Милнера для вывода?)

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

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