[Presentation] Benjamin C. Pierce: Types Considered Harmfull
От: deniok Россия  
Дата: 31.05.08 09:13
Оценка: 88 (7) +1
Очень интересно и с юмором. Выводы:

Mechanical checks of simple properties enormously improve software quality:


Needed: Better ways of integrating these different sorts of checks


ЗЫ: Benjamin C. Pierce, кто не знает, автор Types and Programming Languages — одного из лучших учебников по теории типов.
типы презентация
Re: [Presentation] Benjamin C. Pierce: Types Considered Harm
От: deniok Россия  
Дата: 31.05.08 09:15
Оценка:
Здравствуйте, deniok, Вы писали:

Ссылку-то и забыл
Re: [Presentation] Benjamin C. Pierce: Types Considered Harm
От: Кодт Россия  
Дата: 02.06.08 10:18
Оценка:
Здравствуйте, deniok, Вы писали:

Про линзы всё понятно... А где бананы и колючая проволока?
... << RSDN@Home 1.2.0 alpha rev. 655>>
http://files.rsdn.org/4783/catsmiley.gif Перекуём баги на фичи!
Re: [Presentation] Benjamin C. Pierce: Types Considered Harm
От: Lazy Cjow Rhrr Россия lj://_lcr_
Дата: 02.06.08 18:55
Оценка: +1
deniok,


Из презентации чувствуется, что Пирс полюбил контракты и что контракты ныне наше фсё.

Возьмём простейший стек, и зададимся вопросом: "какие контракты будут у ево методов?". Ответ: примерно такие
Автор: Lazy Cjow Rhrr
Дата: 12.07.06
Получается, что они конечно general, но на практике этот general будет весьма specific

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

И юнит-тесты они тоже конечно specific, но в сочетании с регулярностью самой программы могут быть весьма general, например юнит тест для стека:
testSize()
{
    Stack s1 = new Stack(4);
    assertTrue(s1.size() == 0);
    s1.push("1");
    s1.push("2");
    s1.push("3");
    assertTrue(s1.size() == 3);
    assertExeption(s1.push("4"), Overflow.class); 
}

доказывает не только, что для стека размера 4 будут выполняться эти условия, а это будет доказывать справедливость и для стека произвольного размера n, потому что в соответствии с самим кодом фукций Stack, push и size у нас есть только 3 возможных состояния (пустой, непустой и полный) и мы их все протестили.

Так что, как мне кажется, и типы рано списывать со счетов, и юнит-тесты требуют более пристального теоретического исследования насчёт "free teorems" .
... << RSDN@Home 1.2.0 alpha 4 rev. 1079>>
http://files.rsdn.org/10144/thinker.gif quicksort =: (($:@(<#[),(=#[),$:@(>#[)) ({~ ?@#)) ^: (1<#)
Re: [Presentation] Benjamin C. Pierce: Types Considered Harm
От: vshabanov http://vshabanov-ru.blogspot.com
Дата: 03.06.08 10:07
Оценка:
Здравствуйте, deniok, Вы писали:

D>Очень интересно и с юмором. Выводы:

D>
D>Needed: Better ways of integrating these different sorts of checks

D>[/q]

Вообще мысль забавная: добавить к типам проверки значений и везде, где будет описан нужный тип, проверки вставятся автоматом. Этакие автоматизированные assert-ы. Но все-таки есть ощущение, что ничего нового в этой презентации пока нет, такие же инварианты/контракты, как в Eiffel, только с частичной статической типизацией.
Re[2]: [Presentation] Benjamin C. Pierce: Types Considered H
От: Курилка Россия http://kirya.narod.ru/
Дата: 03.06.08 10:16
Оценка:
Здравствуйте, vshabanov, Вы писали:

V>Вообще мысль забавная: добавить к типам проверки значений и везде, где будет описан нужный тип, проверки вставятся автоматом. Этакие автоматизированные assert-ы. Но все-таки есть ощущение, что ничего нового в этой презентации пока нет, такие же инварианты/контракты, как в Eiffel, только с частичной статической типизацией.


Ну там ссылка есть на работу Хинце с сотоварищами, вполне там контракты эфейлевские, даж помощней (хаскель всёж), плюс с выведением "виноватого".
Хотя так-то это всё то же, и для себе сильно большой выгоды в этом не вижу, разве что баги чуть быстрей находить можно, но есть же квикчек, да и собственный мозг, их никто не отменял вроде
Правда Пирс об обобщении этого всего вроде ратует, правда какое отношение линзы к этому имеют я не вкуриваю.
Re[3]: [Presentation] Benjamin C. Pierce: Types Considered H
От: Lazy Cjow Rhrr Россия lj://_lcr_
Дата: 03.06.08 11:39
Оценка:
Курилка,

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


У quickcheck есть недостаток в том, что распределение тестовых данных нужно формировать самому. Вот если бы оно само делалось в зависимости от того, какие функции вызываются в тестах — мне кажется это было бы нереально круто

Есть работа, где авторы думают примерно в этом направлении ("Unit Tests Reloaded: Parameterized Unit Testing with Symbolic Execution") но немного с другого боку. Нужно только объединить эти два подхода.

А собственный моск наверное лучше использовать на более творческие задачи, ежели написание юнит тестов
... << RSDN@Home 1.2.0 alpha 4 rev. 1079>>
http://files.rsdn.org/10144/thinker.gif quicksort =: (($:@(<#[),(=#[),$:@(>#[)) ({~ ?@#)) ^: (1<#)
Re[4]: [Presentation] Benjamin C. Pierce: Types Considered H
От: Курилка Россия http://kirya.narod.ru/
Дата: 03.06.08 11:44
Оценка:
Здравствуйте, Lazy Cjow Rhrr, Вы писали:

LCR>Курилка,


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


LCR>У quickcheck есть недостаток в том, что распределение тестовых данных нужно формировать самому. Вот если бы оно само делалось в зависимости от того, какие функции вызываются в тестах — мне кажется это было бы нереально круто


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

LCR>Есть работа, где авторы думают примерно в этом направлении ("Unit Tests Reloaded: Parameterized Unit Testing with Symbolic Execution") но немного с другого боку. Нужно только объединить эти два подхода.


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


Ага, я вот решил завязать с программированием
Re[5]: [Presentation] Benjamin C. Pierce: Types Considered H
От: Lazy Cjow Rhrr Россия lj://_lcr_
Дата: 04.06.08 04:17
Оценка:
Курилка,

К>У хинцевских контрактов тож самое, только они выдают ктож сбажил (в рамках разумного, конечно).

К>Т.е. контракт нарушается только в случае его проверки (т.е. конкретного теста)

Не понял, что за зверь?

К>Ага, я вот решил завязать с программированием


Ого! Решил строить студентов? Али квадратики со стрелочками будешь рисовать?
... << RSDN@Home 1.2.0 alpha 4 rev. 1079>>
http://files.rsdn.org/10144/thinker.gif quicksort =: (($:@(<#[),(=#[),$:@(>#[)) ({~ ?@#)) ^: (1<#)
Re[6]: [Presentation] Benjamin C. Pierce: Types Considered H
От: Курилка Россия http://kirya.narod.ru/
Дата: 04.06.08 05:22
Оценка:
Здравствуйте, Lazy Cjow Rhrr, Вы писали:

LCR>Курилка,


К>>У хинцевских контрактов тож самое, только они выдают ктож сбажил (в рамках разумного, конечно).

К>>Т.е. контракт нарушается только в случае его проверки (т.е. конкретного теста)

LCR>Не понял, что за зверь?


Ну вот пишешь, пишешь...
(Эт я и про себя и про Пирса )
Ну глянь здесь

К>>Ага, я вот решил завязать с программированием


LCR>Ого! Решил строить студентов? Али квадратики со стрелочками будешь рисовать?


Да так, скорей админить, но может и студентами когда займусь...
Квадратики со стрелочками тоже уже несколько поднадоели (UML особливо)
 
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.