История изменений
Исправление AndreyKl, (текущая версия) :
Не выкидывает. Она остаётся частью типа результата.
Ну ситуация аналогична. В остальных языках тоже выкидывают если могут.
Кстати, я пошёл и поглядел таки, liquid haskell это похоже действительно зависимые типы, правда внутри (про ликвид хаскель не нашёл, но они на сайте lh дают ссылку на статью ниже, думаю что это основа, собственно). Но всё что применимо к зависимым типам (в смысле разрешимости там и прочих добрых свойств), должно быть применимо и к ликвид хаскель. Единственное, правда, lh может быть более ограниченным, потому что там исходный язык lh переводится в язык зависимых типов. Т.е. исходный язык может быть менее выразительным чем зависимые типы, но я не разбирался там. Правда из цитаты ниже создаётся впечатление что это именно так и есть. Вот статья http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf
вот цитата
We present Logically Qualified Data Types, abbreviated to LiquidTypes, a system that combines Hindley-Milnertype 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.
Всю информацию о типах можно выкинуть на этапе компиляции.
В зависимых типах не всегда получается на практике (а в теории я не помню что там к чему). Но таки в большинстве случаев это работает.
Исправление AndreyKl, :
Не выкидывает. Она остаётся частью типа результата.
Ну ситуация аналогична. В остальных языках тоже выкидывают если могут.
Кстати, я пошёл и поглядел таки, liquid haskell это зависимые типы, правда внутри. Но всё что применимо к зависимым типам (в смысле разрешимости там и прочих добрых свойств), должно быть применимо и к ликвид хаскель. Единственное, правда, lh может быть более ограниченным, потому что там исходный язык lh переводится в язык зависимых типов. Т.е. исходный язык может быть менее выразительным чем зависимые типы, но я не разбирался там. Правда из цитаты ниже создаётся впечатление что это именно так и есть. Вот статья http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf
вот цитата
We present Logically Qualified Data Types, abbreviated to LiquidTypes, a system that combines Hindley-Milnertype 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.
Всю информацию о типах можно выкинуть на этапе компиляции.
В зависимых типах не всегда получается на практике (а в теории я не помню что там к чему). Но таки в большинстве случаев это работает.
Исправление AndreyKl, :
Не выкидывает. Она остаётся частью типа результата.
Ну ситуация аналогична. В остальных языках тоже выкидывают если могут.
Кстати, я пошёл и поглядел таки, liquid haskell это зависимые типы, правда внутри. Но всё что применимо к зависимым типам (в смысле разрешимости там), применимо и к ликвид хаскель. Единственное, правда, lh может быть более ограниченным, потому что там исходный язык lh переводится в язык зависимых типов. Т.е. исходный язык может быть менее выразительным чем зависимые типы, но я не разбирался там. Правда из цитаты ниже создаётся впечатление что это именно так и есть. Вот статья http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf
вот цитата
We present Logically Qualified Data Types, abbreviated to LiquidTypes, a system that combines Hindley-Milnertype 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.
Всю информацию о типах можно выкинуть на этапе компиляции.
В зависимых типах не всегда получается на практике (а в теории я не помню что там к чему). Но таки в большинстве случаев это работает.
Исходная версия AndreyKl, :
Не выкидывает. Она остаётся частью типа результата.
Ну ситуация аналогична. В остальных языках тоже выкидывают если могут.
Кстати, я пошёл и поглядел таки, liquid haskell это зависимые типы, правда внутри. Но всё что применимо к зависимым типам (в смысле разрешимости там), применимо и к ликвид хаскель. Единственное, правда, lh может быть более ограниченным, потому что там исходный язык lh переводится в язык зависимых типов. Т.е. исходный язык может быть менее выразительным чем зависимые типы, но я не разбирался там. Вот статья http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf
вот цитата
We present Logically Qualified Data Types, abbreviated to LiquidTypes, a system that combines Hindley-Milnertype 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.
Всю информацию о типах можно выкинуть на этапе компиляции.
В зависимых типах не всегда получается на практике (а в теории я не помню что там к чему). Но таки в большинстве случаев это работает.