Login  Register

Статическая типизация -- это круто?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
33 messages Options Options
Embed post
Permalink
12
Reply | Threaded
Open this post in threaded view
| More
Print post
Permalink

Re: Статическая типизация -- это круто?

sdfgh153
Ну я об этом и писал, что St пока сохраняет некоторое преимущество только в области среды разработки. С другой стороны очень похоже ситуация складывается с лиспом, который точно так же позволяет работать с "живой системой", однако есть довольно много статически типизированных диалектов[1] и вариантов типизации[2].

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

Именно для этого придумали тесты, кстати. Чтобы следить за непротиворечивостью по мере внесения изменений. Тайпчекер может взять на себя часть этих забот, добавив головняка разработчику, конечно. Но и тесты, в общем-то, создаются чтобы добавить разработчику проблем в том случае, если он что-то делает не так.  Разница только в том, что типы писать сильно проще, чем тесты, которые будут проверять типы.

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

А вот тесты непротиворечивости понятийного аппарата это как раз то, что статика закрывает прекрасно. Чтобы программист по ошибке не перепутал Божий дар с яичницей и муху с котлетой. Такие ошибки, увы, не редкость и статика тут сильно упрощает жизнь.

А в вопросах анализа кода статика как раз только помогает, поэтому если бы получилось сделать статически типизированный St получилась бы просто бомба.

1. http://docs.racket-lang.org/ts-guide/
2. http://en.wikipedia.org/wiki/Qi_%28programming_language%29


2013/7/23 Denis Kudriashov <[hidden email]>
Статическая типизация, по сути, это всего лишь специфический инструмент разработки. При этом статически типизированные языки требуют, обязывают использовать этот инструмент постоянно в процессе программирования. А что этот инструмент реально дает? Действительно ли результат работы этого инструмента повышают эффективность разработки?
Давайте, посмотрим на что мы, разработчики, тратим больше всего времени при программировании.

Процесс разработки - это постоянное изменение системы (создание нового кода - тоже изменение). Когда мне приходит очередная задача, я должен выяснить, как ее встроить в систему, что нужно изменить в текущем дизайне, где эти изменения должны быть сделаны.
Для этого я должен понимать как программа работает. И в результате, больше всего времени я трачу на исследование системы. Что делает конкретный кусок кода? Где он используется? Как он устроен внутри?
То же самое касается поиска багов, что тоже занимает много времени. И здесь я имею в виду не поиск нереализованного метода, а поиск причины, почему 2+2=5.

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

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


23 июля 2013 г., 15:33 пользователь Dmitry Matveev <[hidden email]> написал:
>Ну, или иначе задам вопрос. "Стандартная" (C/++, Java, C#, Pascal и т.д.) статика мне только мешает. Усилия на раннее "приколачивание" типов и дальнейшее поддержание компилятора в удовлетворенном состоянии не оправдывает себя. По крайней мере, с моим стилем разработки, который, наверное, можно охарактеризовать как "agile", или более конкретно назвать TDD.

Да, как правило. Как небольшое исключение, в  С++ (за остальные не скажу) можно тоже выделывать интересные вещи с типами, шаблонами, двухэтажными шаблонами, трёхэтажными шаблонами, и т.д. Но это удел особых акробатов, навроде Александреску и последователей. Тут очень верно подмечена "стандартность" таких систем типов. Как правило, сводится всё к указанию типов используемых переменных (в С++11 появилось auto, ура), и типов объектов, с которыми нам предстоит взаимодействовать.

> Правильная типизация (Haskell & Co.) — оправдывает себя в реальной жизни? Нужно ли менять для этого "мой" стиль (постепенное выяснение требований к системе в процессе ее разработки и даже эксплуатации — все как Бек прописал когда-то, короче)? 

В Haskell типизация выходит (точнее вышла, для меня-темноты) на абсолютно новый уровень. Сейчас попытаюсь объяснить, в чём соль.

В Haskell типы охватывают почти все аспекты внутренней структуры программы. Каждая функция имеет свой тип. Вы скажете, "ну и что, у нас вот в C++/Java/Whatever тоже каждая функция/метод имеют свой тип". Но благодаря чистоте Haskell, грубо говоря, всё, что мы можем сделать в функции, отражено в её типе.

Приведу наболевший пример из своей небольшой, но всё же, практики. По работе мне приходилось поддерживать довольно большие проекты (~ 3 млн строк) на С++. Кто только не прикладывал руку к этим тоннам кода за 10+ лет! О качестве того, что там творилось, лучше не говорить. Порой, когда что-то в очередной раз отвалится (или выяснится, что что-то всегда отваливалось, но мы только заметили), на анализ происходящего в портянках на несколько экранов уходили долгие дни, а то и недели. Что только не делалось в одном отдельно взятом методе, куда только оттуда не обращались, чего оттуда только не модифицировали, перетасовывали, преобразовывали, открывали, закрывали, и так далее. Можно долго размышлять о том, почему разработчик(и) сделали именно так, но в конечном итоге это потому что они просто могут!. Они могут писать такой код, и пишут. И он даже работает, до поры-до времени. Компилятор C++ безропотно переводит этот креатив в машинный код и не предоставляет почти никаких средств для контроля и ограничения за происходящим. Глядя на сигнатуру метода или функции, мы не можем ничего о нём сказать. Обратится ли он к объекту А? Модифицирует ли он объект Б? Полезет ли он в Интернет в процессе работы?

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

Если функция, в прототипе которой обозначено, что она в процессе работы обращается (читает) окружение A (Reader A), мы не сможем из неё вызвать функцию, которая в процессе работы что-то сообщает (пишет) в B (Writer B). И обе они гарантированно не будут обращаться к диску или лезть в Интернет.

Это предоставляет абсолютно иные возможности для контроля целостности абстракций, так сказать. Я был просто в восторге, когда наконец нашёл такой инструмент. "Джва года искал".
Хотя, с другой стороны, бывает, что с компилятором Haskell приходится повоевать, когда его представления о типах не совпадают с нашими. Не самый приятный процесс :)

Выдыхаю,

Дмитрий


23 июля 2013 г., 12:01 пользователь Dennis Schetinin <[hidden email]> написал:

Много раз слышал/читал про "правильную" типизацию, но не нахожу времени, а самое главное — желания (ну, вот не убедили меня пока, что нужно выискивать время и тратить его на изучение этого подхода). Поэтому несколько глупых вопросов?
 
В добавок ко всему, кажется мир наигрался в динамическую типизацию. Я сам пишу на Objective-C большую часть дня. Несмотря на то, что формально там статическая типизация (причем самого низкого пошиба, с аннотациями типов), мне ее мало. Я постоянно натыкаюсь на рантаймовые ошибки в своем коде. Поэтому когда время от времени у меня появляется возможность написать что-нибудь на языке с хорошей статической типизацией (Haskell, ML, Go, Typescript) я радуюсь как ребенок.

Реально, правильная статическая типизация исключает рантаймовые ошибки начисто? 

Ну, или иначе задам вопрос. "Стандартная" (C/++, Java, C#, Pascal и т.д.) статика мне только мешает. Усилия на раннее "приколачивание" типов и дальнейшее поддержание компилятора в удовлетворенном состоянии не оправдывает себя. По крайней мере, с моим стилем разработки, который, наверное, можно охарактеризовать как "agile", или более конкретно назвать TDD. 

Правильная типизация (Haskell & Co.) — оправдывает себя в реальной жизни? Нужно ли менять для этого "мой" стиль (постепенное выяснение требований к системе в процессе ее разработки и даже эксплуатации — все как Бек прописал когда-то, короче)? 

Когда несколько лет назад нас здесь троллил поклонник Haskell-а, он только пел про то, что все замечательно, но как это замечательно получается — я лично так и не понял. Не найдется ли у вас или других (я знаю, такие есть) обладателей глубоких знаний в области правильных (=функциональных? ну, или любых других, которые "превосходят Smalltalk по гибкости") ЯП желания и времени немного порекламировать (обосновано) эти более продвинутые технологии?
 
Smalltalk в этом отношении не сделал никаких толковых шагов с последнего релиза Strongtalk в 2006 году. (Опережая обвинение в пассивности: я глупый, у меня головы не хватит подхватить разработку Strongtalk)
Ну есть еще Василий Быков с Гиладом Брахой, которые тихонечко пилят Newspeak и что-то робко говорят о Pluggable Typesystems. В общем-то там прорывов тоже не ожидается, хотя работа очень интересная.

По этому поводу есть некоторые мысли, но я их пока не буду оглашать — зарезервирую это место на будущее :)

--

Best regards,


Dennis Schetinin

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 
Reply | Threaded
Open this post in threaded view
| More
Print post
Permalink

Re: Статическая типизация -- это круто?

Dennis Schetinin
In reply to this post by semka.novikov
Я понимаю, что такой же тест можно написать на языке со статической типизацией. Я даже вполне допускаю, что аналогичное требование можно описать в типах (хотя, мне кажется, это будет гораздо сложнее того, что я написал — нет?). Вопрос — в том, поможет ли статическая типизация здесь? Другими словами, превысит ли выгода от ее использования связанные с ее использованием "накладные расходы"?

Насчет TDD. В Test-Driven Development существительное — "разработка", а Test (в сочетании с -Driven) — прилагательное. Задача не протестировать систему, а разработать ее. Тесты пишутся для вносимой новой функциональности — вот она (в терминах вариантов использования) "покрывается" тестами на 100%. Но это не означает 100%-е покрытие тестами кода (всех его закоулков, всех возможных сочетаний различных фич и т.д.). Задача — разработать, а не проверить, убедиться в надежности и т.д. Возможно, это всем очевидно, но я раз за разом вижу в высказывания повсюду признаки того, что это до конца не понимается. А по своему опыту я знаю, что понимание этого очень сильно влияет и на практику. По крайней мере, у меня TDD пошло гораздо легче и естественнее именно после осознания этого простого факта.

--

Best regards,


Dennis Schetinin



23 июля 2013 г., 18:58 пользователь <[hidden email]> написал:
Ну, вы написали функциональный тест, его можно написать и на языке со статической типизацией, только он еще будет гарантировать, что в метод remove: of: не передадут вместо количества и продукта, например, экземпляры дебаггера.
 
Кстати если заморочиться, такое можно описать на зависимых типах :)
 
А TDD как раз подразумевает (по своему же определению) написание тестов для всего: Test Driven Development. Об этом сам Бек неоднократно писал.
 
 
От: Dennis Schetinin
Отправлено: вторник, 23 июля 2013 г. 20:33
Кому: Russian Smalltalk User Group
 
Судя по написанным фразам, вы просто "не уловили" суть TDD. Ни о какой 100% test coverage речь не идет. Не надо тестировать все. Не надо тестировать некоторые классы. Вообще ничего тестировать не надо. Надо просто писать код, который показывает как данная программная подсистема должна работать. А это не так сложно. :)

А на самом деле, система вывода сможет мне вывести что-то наподобие этого?

OrderTests >> testRemovesProductFromWarehouseWhenFilled
    [:warehouse | 
        order := Order on: #amount of: #product.
        [order fillFrom: warehouse ] should satisfy: [warehouse remove: #amount of: #product]
    ] runScenario

Здесь записано следующее требование: при выполнении заказа (fillFrom:) соответствующее количество товара списывается со склада (remove:of:). Пример кривоватый, лучше сейчас придумать не успеваю, но, думаю, смысл понятен? Такое требование в типах красиво и легко записывается?




--

Best regards,


Dennis Schetinin



23 июля 2013 г., 15:54 пользователь Semyon Novikov <[hidden email]> написал:
TDD это круто, конечно, но не работает. Только истинные титаны духа могут действительно писать 100% кода по принципу test first. Я пробовал раз шесть, наверное, в итоге скатился к "а вот этот класс можно и потестировать, остальное как-нибудь так". Потому что тесты писать трудно. Если у вас правда получается 100% test coverage, я снимаю шляпу и восхищаюсь.

Типы писать не трудно, они не отдельная сущность, а код, который ты само собой тоже пишешь (или его выводит компилятор, что случается чаще). Нормальная система типов позволяет расслабиться и писать тесты только там, где тайпчекер почему-то не может доказать правильность. Именно поэтому именно в языке с невероятно статической типизацией стал возможен QuickCheck[1], откуда он уже и расползся на все прочие языки.

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

Впрочем прототипы как раз можно писать хоть на джаваскрипте.



2013/7/23 Dennis Schetinin <[hidden email]>

23 июля 2013 г., 14:59 пользователь Semyon Novikov <[hidden email]> написал:

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

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

Но на практике они все равно договариваются, какие именно сообщения будет понимать получатель. Возникает интерфейс. И тут разница внезапно заканчивается. Потому что когда я определяю функции над абстрактным типом данных, я тоже определяю интерфейс. Вся разница в том, что:
  1. Интерфейс задокументирован
  2. Соответствие кода интерфейсам проверяется компилятором
То есть шанс того, что мой коллега напишет код, который скомпилируется, но приведет к ошибке во время исполнения минимален. Логика работы контролируется тайпчекером.

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

Это все прекрасно покрывается TDD (в ее полном воплощении, то есть когда "классику" предваряет построение "сверху-вниз" с помощью моков. Причем на выходе получается не отдельно код и отдельно система типов, а только один сплошной код ("реализация" и "тесты"). Другое дело, что весь потенциал этого подхода до сих пор не раскрыт… Но это отдельный разговор… Как и то, что здесь как раз виднеется "смыкание" обоих подходов: код ведь тоже поддается анализу, и аннотации к коду (разновидностью которых являются типы) тоже могут быть записаны в виде кода…

Но возвращаясь к теме, замечу, что преимущество динамики проявляется в возможности состряпать "наполовину пропеченную" систему. Если я хочу проверить какую-то идею (пара минут на написание кода и встраивание его в одно нужное место и еще пара на просмотр того, как она себя ведет в этом одном месте), то мне обычно как-то не хочется тратить еще 15 минут на то, чтобы умилостивить систему типизации, так как нужный кусок кода (потом) будет встраиваться еще в 100500 мест. Поскольку при моем подходе такие исследования занимают много времени (не сказать, что построение системы из них и состоит: берется требование, придумывается простенькое решение, проверяется как оно ложится на существующую систему и т.д.…), накладные расходы на уговаривание компилятора здесь весьма существенны. Как с этим обстоит дело в правильных языках?
 
Ну и вы так пишете о арифметике в St, будто она не поломала мозг тысячам ни в чем неповинных программистов :) Она там как раз неестественна, тот случай, когда предметную область изуродовали в угоду особенностям синтаксиса. Не могу этого одобрить.

А о чем конкретно речь? Если исключительно о синтаксисе, то я бы сказал, что вся проблема в том, что человечество говорит на двух языках: человеческом и математическом. И именно неестественность математического языка здесь проявляет себя, поэтому приходится выбирать, что лучше: оставить систему простой и человеческой или же "умилостивить" математиков. Я лично очень рад, что создатели Smalltalk-а выбрали первый путь.

Если же разговор о реализации и о том, "как все устроено", то было бы интересно узнать, о каких именно уродствах речь?
 
 
А все прочие чудесные вещи прекрасно реализуются и в статически-типизированных языках, я о бесконечной точности и. т.п[1]

1. http://www.haskell.org/haskellwiki/Libraries_and_tools/Mathematics



2013/7/23 Nikolay Kleptsov <[hidden email]>
Посылка сообщения в Smalltalk предполагает, что имеется ссылка на получателя (не обязательно определенного типа), селектор и аргументы сообщения. В качестве получателя может быть любой объект. Тело сообщения может быть любым. В этом и состоит основное преимущество.
Например, числовая арифметика изящно реализована в Smalltalk. Автоматическое преобразование типов. Наличие чисел "абсолютной" точности.
Насчет типизации в Dolphin предложили интересное решение - реализация необходимого протокола.


23 июля 2013 г., 14:29 пользователь Semyon Novikov <[hidden email]> написал:

Никакая типизация не может защитить от электрика и ошибки ввода-вывода. Поэтому нет, конечно не начисто, но довольно близко. То есть если ваша программа на Haskell (или еще чем-нибудь еще более суровом типа Idris или Agda) скомпилировалась, то скорее всего она будет работать корректно в рамках той модели, которую вы там напрограммировали. Статика позволяет удостовериться, что вы в рамках собственного воображаемого мирка из данных и преобразований над ними делаете все как минимум непротиворечиво. Это дорогого стоит, кстати. Потому что вы можете на этапе компиляции найти архитектурную ошибку. Эдакий лихой способ больше думать о предметной области и меньше о коде, мне нравится.

Разработка "от типов" не исключает мелкие итерации и TDD, просто вы начинаете с описания типов. Они могут меняться, удаляться или появляться со временем, точно так же как в любой другой системе. Причем если вы поменяете тип и у вас все развалится, то оно развалится на этапе проверки типов, а не в рантайме. Еще приятным момент, что развалится везде, где может развалиться в принципе. Не надо рыскать по приложению и искать ошибки типизации в рантайме.

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

А "стандартная" наивная статическая типизация действительно часто мешает больше, чем помогает. Но я говорю о чуть более сложных вещах, о выводе типов, как минимум. Кому нравится писать эти жуткие аннотации? Компилятор их выведет сам (в большей или меньшей степени). А если это не примитивный вывод типов а-ля Go или Typescript, то оно еще и завершаемость проверит и валидность доказуемых высказываний, и еще много чего.

На Хаскеле писать очень приятно, я сам в продакшн ничего не писал, но знаю, что люди пишут с большим успехом (http://bazqux.com, например, написан на нем). Из статически типизированных языков я использую Go и Typescript. Они ближе к "традиционной статике", но умеют выводить типы выражений, что сильно облегчает работу.

Того хаскелиста я помню, но я не ставлю целью никого троллить, я люблю St, но у меня к нему сложное отношение.

Про Новояз послушал бы с удовольствием, не томи :))


From: [hidden email]
Date: Tue, 23 Jul 2013 12:01:44 +0400
Subject: [RSUG] Статическая типизация -- это круто?
To: [hidden email]


Много раз слышал/читал про "правильную" типизацию, но не нахожу времени, а самое главное — желания (ну, вот не убедили меня пока, что нужно выискивать время и тратить его на изучение этого подхода). Поэтому несколько глупых вопросов?
 
В добавок ко всему, кажется мир наигрался в динамическую типизацию. Я сам пишу на Objective-C большую часть дня. Несмотря на то, что формально там статическая типизация (причем самого низкого пошиба, с аннотациями типов), мне ее мало. Я постоянно натыкаюсь на рантаймовые ошибки в своем коде. Поэтому когда время от времени у меня появляется возможность написать что-нибудь на языке с хорошей статической типизацией (Haskell, ML, Go, Typescript) я радуюсь как ребенок.

Реально, правильная статическая типизация исключает рантаймовые ошибки начисто? 

Ну, или иначе задам вопрос. "Стандартная" (C/++, Java, C#, Pascal и т.д.) статика мне только мешает. Усилия на раннее "приколачивание" типов и дальнейшее поддержание компилятора в удовлетворенном состоянии не оправдывает себя. По крайней мере, с моим стилем разработки, который, наверное, можно охарактеризовать как "agile", или более конкретно назвать TDD. 

Правильная типизация (Haskell & Co.) — оправдывает себя в реальной жизни? Нужно ли менять для этого "мой" стиль (постепенное выяснение требований к системе в процессе ее разработки и даже эксплуатации — все как Бек прописал когда-то, короче)? 

Когда несколько лет назад нас здесь троллил поклонник Haskell-а, он только пел про то, что все замечательно, но как это замечательно получается — я лично так и не понял. Не найдется ли у вас или других (я знаю, такие есть) обладателей глубоких знаний в области правильных (=функциональных? ну, или любых других, которые "превосходят Smalltalk по гибкости") ЯП желания и времени немного порекламировать (обосновано) эти более продвинутые технологии?
 
Smalltalk в этом отношении не сделал никаких толковых шагов с последнего релиза Strongtalk в 2006 году. (Опережая обвинение в пассивности: я глупый, у меня головы не хватит подхватить разработку Strongtalk)
Ну есть еще Василий Быков с Гиладом Брахой, которые тихонечко пилят Newspeak и что-то робко говорят о Pluggable Typesystems. В общем-то там прорывов тоже не ожидается, хотя работа очень интересная.
По этому поводу есть некоторые мысли, но я их пока не буду оглашать — зарезервирую это место на будущее :)
--
Best regards,


Dennis Schetinin

--

Best regards,


Dennis Schetinin

 

 

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 

 

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 

 

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 
Reply | Threaded
Open this post in threaded view
| More
Print post
Permalink

Re: Статическая типизация -- это круто?

Denis Kudriashov
In reply to this post by sdfgh153
24 июля 2013 г., 8:38 пользователь Semyon Novikov <[hidden email]> написал:
А в вопросах анализа кода статика как раз только помогает, поэтому если бы получилось сделать статически типизированный St получилась бы просто бомба.

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

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 
Reply | Threaded
Open this post in threaded view
| More
Print post
Permalink

Re: Статическая типизация -- это круто?

Dmitry Matveev
Ну не может этого быть достаточно для эффективной разработки крупной системы, для ее поддержки, для ее изучения новыми программистами (конечно, знающими язык). И в этом смысле смолтолк-подобные среды на порядок превосходят остальные технологии. 

Тем не менее, большинство крупных систем сегодня написано как раз не на смолтоке*. Sad but true.

Дмитрий

*Java IDE относятся к смолток-подобным средам?


24 июля 2013 г., 10:27 пользователь Denis Kudriashov <[hidden email]> написал:
24 июля 2013 г., 8:38 пользователь Semyon Novikov <[hidden email]> написал:

А в вопросах анализа кода статика как раз только помогает, поэтому если бы получилось сделать статически типизированный St получилась бы просто бомба.

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

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 
Reply | Threaded
Open this post in threaded view
| More
Print post
Permalink

Re: Статическая типизация -- это круто?

Denis Kudriashov
24 июля 2013 г., 10:34 пользователь Dmitry Matveev <[hidden email]> написал:
Ну не может этого быть достаточно для эффективной разработки крупной системы, для ее поддержки, для ее изучения новыми программистами (конечно, знающими язык). И в этом смысле смолтолк-подобные среды на порядок превосходят остальные технологии. 

Тем не менее, большинство крупных систем сегодня написано как раз не на смолтоке*. Sad but true.

Дмитрий

*Java IDE относятся к смолток-подобным средам?

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

 


24 июля 2013 г., 10:27 пользователь Denis Kudriashov <[hidden email]> написал:
24 июля 2013 г., 8:38 пользователь Semyon Novikov <[hidden email]> написал:

А в вопросах анализа кода статика как раз только помогает, поэтому если бы получилось сделать статически типизированный St получилась бы просто бомба.

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

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 
Reply | Threaded
Open this post in threaded view
| More
Print post
Permalink

Re: Статическая типизация -- это круто?

sdfgh153
In reply to this post by Denis Kudriashov
Например Lexah[1]. Там чрезвычайно дофига навигации и метаинформации взятой из системы типов.
Если не брать в расчет конкретно хаскель, то есть Visual Studio F#, там тоже все хорошо с использованием системы типов.
Вся навигация для Typescript в Visual Studio (и в игрушечном веб-редакторе[2] тоже) основана на типах.

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

Впрочем я вообще лучший свой софт написал в vi, acme или sam даже без подсветки синтаксиса[3]. Используя grep и здравй смысл для навигации. Честное слово, мне это нравится больше любого IDE, даже смолтокового. Я понимаю, что это подходит не всем.

К слову один из самых крупных и сложных проектов современности написан на Си в микроемаксе — это ядро Linux.

По сути Смолток очень подкупает именно тем, что это живая система. Навскидку я такое могу вспомнить только в лиспе. Но, как я уже упоминал, есть статически типизированные лиспы. Живые. А вот живых статически типизированных смолтоков, к сожалению, нет.


2013/7/24 Denis Kudriashov <[hidden email]>
24 июля 2013 г., 8:38 пользователь Semyon Novikov <[hidden email]> написал:

А в вопросах анализа кода статика как раз только помогает, поэтому если бы получилось сделать статически типизированный St получилась бы просто бомба.

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

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 
Reply | Threaded
Open this post in threaded view
| More
Print post
Permalink

Re: Re[2]: [RSUG] СтатичеÑ�кая типизация -- это круто?

semka.novikov
In reply to this post by Igor Stasenko
Так, я наверное должен извиниться за свое косноязычие и неумение донести мысль.
Попробую исправить ситуацию :)
 
Тут множество раз упоминались аннотации типов, как минус статической типизации, сведение выбора static vs. dynamic к “вкусовщине”, аппеляции к трудности вкорячивания статики в парадигму живой системы Smalltalk и много еще чего. Во всем этом виноват я, на самом деле, потому что не смог толком объяснить, что же я имею в виду, когда говорю о статически-типизированном диалекте Smalltalk.
 
Сразу оговорюсь насчет двух вещей:
  • Я люблю Smalltalk и не собираюсь никого троллить.
  • Я не говорю, что статическая типизация должна стать частью именно Smalltalk, я был бы рад видеть другой язык, со статической типизацией и наследующий от Smtalltalk
 
Что вообще такое статическая типизация
 
Как выяснилось у нас уже на этом месте начинается непонимание. Для разнообразия можно почитать определение в википедии[1]:
 
Static type-checking is the process of verifying the type safety of a program based on analysis of a program's text (source code). If a program passes a static type-checker, then the program is guaranteed to satisfy some set of type-safety properties for all possible inputs.
 
То есть статическая типизация это таки действительно процесс, не относящийся к компиляции напрямую. Это именно статический анализ кода. Он выполняется до компиляции и основной целью этого процесса является не доказательство корректной работы логики программы, но только и только доказательство ее типобезопасности[2]. Да, можно и валидность доказывать и быстродействие улучшать, но это все побочные эффекты.
 
На самом примитивном уровне типобезопасность означает только невозможность (без вмешательства аппаратных сбоев) выполнить код, который приведет к ошибке работы с типами. А типы есть всегда, явно или не явно. Понятное дело, что на уровне машинных кодов есть только байты, но хотя бы на уровень выше уже появляются типы.  Smalltalk тут не исключение, кроме того, как было справедливо замечено, он еще и “строго типизирован”. То есть он не “прощает” ошибки типов, просто он проверку делает в рантайме. Чтобы убедиться сделайте так: 42 at:0. 
 
На свете есть ”безтиповые языки” типа Tcl, но это небольшое лукавство, потому что тип там все-таки есть, просто он один: строка. 
 
Но на этом примитивном уровне статическая типизация не заканчивается, о последствиях чуть позже.
 
По поводу “невозможности реализации статической типизации в рамках St”. Честно говоря я не вижу никаких проблем, для того чтобы доказать типобезопасность чего-либо нужно взять произвольный кусок это чего-то и пройтись по нему тайп-чекером. Не важно что это, программа целиком, метод или выражение.
 
Например выражение “head” + “tail” не требует никакого контекста для того, чтобы пройти проверку типов. В случае с Smtalltalk все может быть даже лучше, чем в случае с прочими жалкими языками: нагрузка на тайпчекер минимальна. Каждый раз, когда вы компилируете метод он проверит его и, что важно, запомнит результат. Так что когда вы будете компилировать другой метод, который вызывает уже проверенный, можно будет сэкономить тайпчекеру время.
 
Никто не любит писать аннотации типов
 
Итак, бонус статической типизации: раннее выявление глупых ошибок работы с типизированными значениями. Такие ошибки появляются в любом языке уровнем чуть повыше плинтуса^W машинного кода. Так что подобная проверка имеет право на жизнь, потому что многие такие ошибки в динамических системах умеют прятаться по закоулкам и вылезать уже у заказчика. Статическая типизация позволяет поймать их все разом и на ранних этапах разработки. Но за это она заставляет программиста писать аннотации типов. Никто не любит писать аннотации типов, ну, в самом деле. Кто любит печатать на этой ужасной клавиатуре? Поэтому я готов прямо за всех сторонников статической типизации сейчас сказать: нас тоже бесит писать static public int.
 
О вкусах к типам
 
Сейчас придется немножко перескочить от нежелания писать аннотации типов к опровержению тезиса о том, что любовь к статической проверке типов это именно склонность личности мазохизму.
 
Дело в том, что статическая типизация бывает разной. Бывает та, что в C++, которая заставляет программиста быть белкой с этой картинки: http://dobrokot.ru/pics/nya2010-02-16__00-39-04_114kb.jpg
 
Но вообще-то работа над системами типизации началась чуть ли не раньше, чем возникло само понятие “типизированный язык программирования”. Я говорю о типизированном лямбда исчислении[3], работу над которым начал еще в 30-ых годах Алонзо Черч. Дальше эта самая типизированная лямбда очень хорошо развивалась многими математиками мира и, внезапно, на данный момент мы имеем целых восемь систем типизированной лямбды, которые выстраиваются в симпатичный лямбда-куб[4]. Ну и вообще с тех пор возникла теория типов[5], которая открыла многие интересные особенности типизированных исчислений.
 
Для создания вау-фактора: совсем недавно группа математиков выпустила книгу “Homotopy Type Theory”[6][7], которая грозит подвести новый базис вообще под всю математику. И эта работа очевидным образом относится к теории типов.  (А писали они ее на гитхабе, кстати, что само по себе очень круто)
 
У теории типов огромное количество прикладных моментов, например система типов Хиндли-Милнера[7] используемая в языках семейста ML (Standart ML, Ocaml, F#, Haskell), зависмые типы[8] (Agda, Coq,  Idris, F*).
 
В общем, к чему я все это рассказываю: под статической проверкой типов лежит отнюдь не “вкус к мазохизму”, а математика. Некоторые системы типов, например, Тьюринг-полны[9]. То есть используя такую систему типов можно решить любую в принципе решаемую задачу.
 
Системы типов, которые стоят выше “наивных систем типов” в духе C++, в силу огромного мат-аппарата открывают возможности не только ловить ошибки типизации, но и доказывать валидность, завершаемость[10], непротиворечивость самого кода.
 
Но с ними есть одна проблема: они доказаны только относительно базиса в виде типизированной лямбды. Наши “обычные” языки, как правило, не основаны на лямбда-исчислении. Поэтому все бонусы нам по-прежнему доступны не в полном объеме.
 
Ну и при чем тут аннотации типов?
 
В рамках теории типов, кроме множества других высоколобых штук, разработаны механизмы вывода типов[11]. То есть компилятор выводит тип выражения сам, а не потому, что у выражения этот тип прописан явным образом. К счастью вот вывод типов уже научились худо-бедно реализовывать в императивных языках. Например auto в новом C++ во время компиляции вычислит тип. Var в .net и тому подобное. Есть языки, которые зашли достаточно далеко, например Typescript от Microsoft, Go, D.
 
Понятное дело, что для вывода типов в агрессивной для голой математики среде императивной программы, тайпчекеру нужны “зацепки”. То есть декларации типов писать все равно придется, но в разы меньше, чем можно было себе представить.
 
function append42(x: string) {
var tmp = “42”
return x + tmp
}
 
Это программа на Typescript, которая автоматически выведет тип переменной tmp и всего выражения. То есть вызвать append42(“hello”) будет можно, а вот append42(42) вызовет у компилятора неприязнь, так как он точно знает, что append42 принимает и возвращает строки, хотя у функции нет явной аннотации типа. Пример надуманный, но основную мысль передает.
 
В Smalltalk, когда вы посылаете классу сообщение subclass: вы фактически пишете аннотацию типа. И это уже зацепка для тайпчекера. Впрочем я бы сейчас не хотел углубляться в мечтания о том, как мог бы выглядеть St со статическим выводом типов. Я глупый, пусть про это Браха думает.
 
Резюмирую
 
  1. Статическая типизация это не прихоть и не фантазия, это bulletproof математика. К сожалению такого же уровня научных работ в рамках динамической типизации (и, кстати, ООП в целом) почему-то нет. Не думаю, что никто не пытался.
  2. В современных системах с выводом типов количество раздражающих аннотаций в разы меньше, чем раньше. И писать их просто.
  3. Статическая типизация позволяет реально повысить качество как кода, так и архитектуры, вплоть до доказательства валидности алгоритма
 
Мне кажется все это вполне приятные вещи, которые я был бы просто счастлив увидеть в системе, “под капотом” которой находится Smalltalk с его концепцией “живой системы”, удивительным IDE и много еще чем :)
 
Хочется еще написать о тех случаях, когда динамика действительно удобна и как такие вещи реализуются в системах со статической типизацией, но очень устали пальцы, да и литературу почитать надо. Так что в следующий раз, наверное.
 
 

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 
Reply | Threaded
Open this post in threaded view
| More
Print post
Permalink

Re: Статическая типизация -- это круто?

HandleX
In reply to this post by Dennis Schetinin
А вот многие, говорящие про статическую типизацию, ещё имеют ввиду и последующую скорость исполнения? Т.е. у статической типизации два действующих фактора: анализ кода и последующая скорость работы в тех местах, где компилятор увидит примитивные типы, укладывающиеся в регистры процессора и станет использовать мощные низкоуровневые инструкции для работы с ними.

Однако, выполнение смоллтоком за какие-то миллисекунды "1024 factorial" заставляет задуматься над нужностью типизации и испытать гордость за Smalltalk и его создателей, реализовавших там самую чудесную математику, которую я когда-либо видел. Здесь программисту дана значительная свобода в реализации своих решений, можно не понимать подкапотное строение компьютера, и в то же время решать задачи без боязни переполнить объявленную переменную, например.

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 
Reply | Threaded
Open this post in threaded view
| More
Print post
Permalink

Re: Статическая типизация -- это круто?

sdfgh153
Скажите, а вы получили мое здоровенное письмо с пояснениями?


2013/7/31 HandleX <[hidden email]>
А вот многие, говорящие про статическую типизацию, ещё имеют ввиду и последующую скорость исполнения? Т.е. у статической типизации два действующих фактора: анализ кода и последующая скорость работы в тех местах, где компилятор увидит примитивные типы, укладывающиеся в регистры процессора и станет использовать мощные низкоуровневые инструкции для работы с ними.

Однако, выполнение смоллтоком за какие-то миллисекунды "1024 factorial" заставляет задуматься над нужностью типизации и испытать гордость за Smalltalk и его создателей, реализовавших там самую чудесную математику, которую я когда-либо видел. Здесь программисту дана значительная свобода в реализации своих решений, можно не понимать подкапотное строение компьютера, и в то же время решать задачи без боязни переполнить объявленную переменную, например.

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 
Reply | Threaded
Open this post in threaded view
| More
Print post
Permalink

Re: Статическая типизация -- это круто?

Igor Stasenko
2013/7/31 Semyon Novikov <[hidden email]>:
> Скажите, а вы получили мое здоровенное письмо с пояснениями?
>
я да :)

>
> 2013/7/31 HandleX <[hidden email]>
>>
>> А вот многие, говорящие про статическую типизацию, ещё имеют ввиду и
>> последующую скорость исполнения? Т.е. у статической типизации два
>> действующих фактора: анализ кода и последующая скорость работы в тех местах,
>> где компилятор увидит примитивные типы, укладывающиеся в регистры процессора
>> и станет использовать мощные низкоуровневые инструкции для работы с ними.
>>
>> Однако, выполнение смоллтоком за какие-то миллисекунды "1024 factorial"
>> заставляет задуматься над нужностью типизации и испытать гордость за
>> Smalltalk и его создателей, реализовавших там самую чудесную математику,
>> которую я когда-либо видел. Здесь программисту дана значительная свобода в
>> реализации своих решений, можно не понимать подкапотное строение компьютера,
>> и в то же время решать задачи без боязни переполнить объявленную переменную,
>> например.
>>
>> --
>> --
>> http://groups.google.ru/group/sugr
>> ---
>> Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk
>> User Group.
>>
>> Чтобы отказаться от подписки на эту группу и перестать получать из нее
>> сообщения, отправьте электронное письмо на адрес
>> [hidden email].
>> Настройки подписки и доставки писем:
>> https://groups.google.com/groups/opt_out.
>>
>>
>
>
> --
> --
> http://groups.google.ru/group/sugr
> ---
> Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk
> User Group.
>
> Чтобы отказаться от подписки на эту группу и перестать получать из нее
> сообщения, отправьте электронное письмо на адрес
> [hidden email].
> Настройки подписки и доставки писем:
> https://groups.google.com/groups/opt_out.
>
>



--
Best regards,
Igor Stasenko.

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.

Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.


Reply | Threaded
Open this post in threaded view
| More
Print post
Permalink

Re: Статическая типизация -- это круто?

sdfgh153
Хоть бы крякнули что-нибудь, я же волнуюсь!
Я просто писал-писал, и тут опять двадцать пять — статическая типизация и быстродействие. У меня чуть монокль от неожиданности не выпал.


2013/7/31 Igor Stasenko <[hidden email]>
2013/7/31 Semyon Novikov <[hidden email]>:
> Скажите, а вы получили мое здоровенное письмо с пояснениями?
>
я да :)

>
> 2013/7/31 HandleX <[hidden email]>
>>
>> А вот многие, говорящие про статическую типизацию, ещё имеют ввиду и
>> последующую скорость исполнения? Т.е. у статической типизации два
>> действующих фактора: анализ кода и последующая скорость работы в тех местах,
>> где компилятор увидит примитивные типы, укладывающиеся в регистры процессора
>> и станет использовать мощные низкоуровневые инструкции для работы с ними.
>>
>> Однако, выполнение смоллтоком за какие-то миллисекунды "1024 factorial"
>> заставляет задуматься над нужностью типизации и испытать гордость за
>> Smalltalk и его создателей, реализовавших там самую чудесную математику,
>> которую я когда-либо видел. Здесь программисту дана значительная свобода в
>> реализации своих решений, можно не понимать подкапотное строение компьютера,
>> и в то же время решать задачи без боязни переполнить объявленную переменную,
>> например.
>>
>> --
>> --
>> http://groups.google.ru/group/sugr
>> ---
>> Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk
>> User Group.
>>
>> Чтобы отказаться от подписки на эту группу и перестать получать из нее
>> сообщения, отправьте электронное письмо на адрес
>> [hidden email].
>> Настройки подписки и доставки писем:
>> https://groups.google.com/groups/opt_out.
>>
>>
>
>
> --
> --
> http://groups.google.ru/group/sugr
> ---
> Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk
> User Group.
>
> Чтобы отказаться от подписки на эту группу и перестать получать из нее
> сообщения, отправьте электронное письмо на адрес
> [hidden email].
> Настройки подписки и доставки писем:
> https://groups.google.com/groups/opt_out.
>
>



--
Best regards,
Igor Stasenko.

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.

Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.



--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 
Reply | Threaded
Open this post in threaded view
| More
Print post
Permalink

Re: Re[2]: [RSUG] СтатичеÑ�кая типизация -- это круто?

Igor Stasenko
In reply to this post by semka.novikov
2013/7/28  <[hidden email]>:

> Так, я наверное должен извиниться за свое косноязычие и неумение донести
> мысль.
> Попробую исправить ситуацию :)
>
> Тут множество раз упоминались аннотации типов, как минус статической
> типизации, сведение выбора static vs. dynamic к "вкусовщине", аппеляции к
> трудности вкорячивания статики в парадигму живой системы Smalltalk и много
> еще чего. Во всем этом виноват я, на самом деле, потому что не смог толком
> объяснить, что же я имею в виду, когда говорю о статически-типизированном
> диалекте Smalltalk.
>
> Сразу оговорюсь насчет двух вещей:
>
> Я люблю Smalltalk и не собираюсь никого троллить.
> Я не говорю, что статическая типизация должна стать частью именно Smalltalk,
> я был бы рад видеть другой язык, со статической типизацией и наследующий от
> Smtalltalk
>
>
> Что вообще такое статическая типизация
>
> Как выяснилось у нас уже на этом месте начинается непонимание. Для
> разнообразия можно почитать определение в википедии[1]:
>
>
> Static type-checking is the process of verifying the type safety of a
> program based on analysis of a program's text (source code). If a program
> passes a static type-checker, then the program is guaranteed to satisfy some
> set of type-safety properties for all possible inputs.
>
>
> То есть статическая типизация это таки действительно процесс, не относящийся
> к компиляции напрямую. Это именно статический анализ кода. Он выполняется до
> компиляции и основной целью этого процесса является не доказательство
> корректной работы логики программы, но только и только доказательство ее
> типобезопасности[2]. Да, можно и валидность доказывать и быстродействие
> улучшать, но это все побочные эффекты.
>
> На самом примитивном уровне типобезопасность означает только невозможность
> (без вмешательства аппаратных сбоев) выполнить код, который приведет к
> ошибке работы с типами. А типы есть всегда, явно или не явно. Понятное дело,
> что на уровне машинных кодов есть только байты, но хотя бы на уровень выше
> уже появляются типы.  Smalltalk тут не исключение, кроме того, как было
> справедливо замечено, он еще и "строго типизирован". То есть он не "прощает"
> ошибки типов, просто он проверку делает в рантайме. Чтобы убедиться сделайте
> так: 42 at:0.
>
> На свете есть "безтиповые языки" типа Tcl, но это небольшое лукавство,
> потому что тип там все-таки есть, просто он один: строка.
>
> Но на этом примитивном уровне статическая типизация не заканчивается, о
> последствиях чуть позже.
>
> По поводу "невозможности реализации статической типизации в рамках St".
> Честно говоря я не вижу никаких проблем, для того чтобы доказать
> типобезопасность чего-либо нужно взять произвольный кусок это чего-то и
> пройтись по нему тайп-чекером. Не важно что это, программа целиком, метод
> или выражение.
>
> Например выражение "head" + "tail" не требует никакого контекста для того,
> чтобы пройти проверку типов. В случае с Smtalltalk все может быть даже
> лучше, чем в случае с прочими жалкими языками: нагрузка на тайпчекер
> минимальна. Каждый раз, когда вы компилируете метод он проверит его и, что
> важно, запомнит результат. Так что когда вы будете компилировать другой
> метод, который вызывает уже проверенный, можно будет сэкономить тайпчекеру
> время.
>
> Никто не любит писать аннотации типов
>
> Итак, бонус статической типизации: раннее выявление глупых ошибок работы с
> типизированными значениями. Такие ошибки появляются в любом языке уровнем
> чуть повыше плинтуса^W машинного кода. Так что подобная проверка имеет право
> на жизнь, потому что многие такие ошибки в динамических системах умеют
> прятаться по закоулкам и вылезать уже у заказчика. Статическая типизация
> позволяет поймать их все разом и на ранних этапах разработки. Но за это она
> заставляет программиста писать аннотации типов. Никто не любит писать
> аннотации типов, ну, в самом деле. Кто любит печатать на этой ужасной
> клавиатуре? Поэтому я готов прямо за всех сторонников статической типизации
> сейчас сказать: нас тоже бесит писать static public int.
>
> О вкусах к типам
>
> Сейчас придется немножко перескочить от нежелания писать аннотации типов к
> опровержению тезиса о том, что любовь к статической проверке типов это
> именно склонность личности мазохизму.
>
> Дело в том, что статическая типизация бывает разной. Бывает та, что в C++,
> которая заставляет программиста быть белкой с этой картинки:
> http://dobrokot.ru/pics/nya2010-02-16__00-39-04_114kb.jpg
>
> Но вообще-то работа над системами типизации началась чуть ли не раньше, чем
> возникло само понятие "типизированный язык программирования". Я говорю о
> типизированном лямбда исчислении[3], работу над которым начал еще в 30-ых
> годах Алонзо Черч. Дальше эта самая типизированная лямбда очень хорошо
> развивалась многими математиками мира и, внезапно, на данный момент мы имеем
> целых восемь систем типизированной лямбды, которые выстраиваются в
> симпатичный лямбда-куб[4]. Ну и вообще с тех пор возникла теория типов[5],
> которая открыла многие интересные особенности типизированных исчислений.
>
> Для создания вау-фактора: совсем недавно группа математиков выпустила книгу
> "Homotopy Type Theory"[6][7], которая грозит подвести новый базис вообще под
> всю математику. И эта работа очевидным образом относится к теории типов.  (А
> писали они ее на гитхабе, кстати, что само по себе очень круто)
>
> У теории типов огромное количество прикладных моментов, например система
> типов Хиндли-Милнера[7] используемая в языках семейста ML (Standart ML,
> Ocaml, F#, Haskell), зависмые типы[8] (Agda, Coq,  Idris, F*).
>
> В общем, к чему я все это рассказываю: под статической проверкой типов лежит
> отнюдь не "вкус к мазохизму", а математика. Некоторые системы типов,
> например, Тьюринг-полны[9]. То есть используя такую систему типов можно
> решить любую в принципе решаемую задачу.
>
> Системы типов, которые стоят выше "наивных систем типов" в духе C++, в силу
> огромного мат-аппарата открывают возможности не только ловить ошибки
> типизации, но и доказывать валидность, завершаемость[10], непротиворечивость
> самого кода.
>
> Но с ними есть одна проблема: они доказаны только относительно базиса в виде
> типизированной лямбды. Наши "обычные" языки, как правило, не основаны на
> лямбда-исчислении. Поэтому все бонусы нам по-прежнему доступны не в полном
> объеме.
>
> Ну и при чем тут аннотации типов?
>
> В рамках теории типов, кроме множества других высоколобых штук, разработаны
> механизмы вывода типов[11]. То есть компилятор выводит тип выражения сам, а
> не потому, что у выражения этот тип прописан явным образом. К счастью вот
> вывод типов уже научились худо-бедно реализовывать в императивных языках.
> Например auto в новом C++ во время компиляции вычислит тип. Var в .net и
> тому подобное. Есть языки, которые зашли достаточно далеко, например
> Typescript от Microsoft, Go, D.
>
> Понятное дело, что для вывода типов в агрессивной для голой математики среде
> императивной программы, тайпчекеру нужны "зацепки". То есть декларации типов
> писать все равно придется, но в разы меньше, чем можно было себе
> представить.
>
>
> function append42(x: string) {
>
> var tmp = "42"
> return x + tmp
>
> }
>
>
> Это программа на Typescript, которая автоматически выведет тип переменной
> tmp и всего выражения. То есть вызвать append42("hello") будет можно, а вот
> append42(42) вызовет у компилятора неприязнь, так как он точно знает, что
> append42 принимает и возвращает строки, хотя у функции нет явной аннотации
> типа. Пример надуманный, но основную мысль передает.
>
> В Smalltalk, когда вы посылаете классу сообщение subclass: вы фактически
> пишете аннотацию типа. И это уже зацепка для тайпчекера. Впрочем я бы сейчас
> не хотел углубляться в мечтания о том, как мог бы выглядеть St со
> статическим выводом типов. Я глупый, пусть про это Браха думает.
>
> Резюмирую
>
>
> Статическая типизация это не прихоть и не фантазия, это bulletproof
> математика. К сожалению такого же уровня научных работ в рамках динамической
> типизации (и, кстати, ООП в целом) почему-то нет. Не думаю, что никто не
> пытался.
> В современных системах с выводом типов количество раздражающих аннотаций в
> разы меньше, чем раньше. И писать их просто.
> Статическая типизация позволяет реально повысить качество как кода, так и
> архитектуры, вплоть до доказательства валидности алгоритма
>
>
> Мне кажется все это вполне приятные вещи, которые я был бы просто счастлив
> увидеть в системе, "под капотом" которой находится Smalltalk с его
> концепцией "живой системы", удивительным IDE и много еще чем :)
>
> Хочется еще написать о тех случаях, когда динамика действительно удобна и
> как такие вещи реализуются в системах со статической типизацией, но очень
> устали пальцы, да и литературу почитать надо. Так что в следующий раз,
> наверное.
>
>
>
> http://en.wikipedia.org/wiki/Type_safety
> http://en.wikipedia.org/wiki/Typed_lambda_calculus
> http://ru.wikipedia.org/wiki/%D0%9B%D1%8F%D0%BC%D0%B1%D0%B4%D0%B0-%D0%BA%D1%83%D0%B1
> http://en.wikipedia.org/wiki/Type_theory
> https://github.com/HoTT/book
> http://www.math.ias.edu/sp/univalent
> https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner
> https://en.wikipedia.org/wiki/Dependent_type
> http://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/
> https://en.wikipedia.org/wiki/Halting_Problem
> https://en.wikipedia.org/wiki/Type_inference
>
> --
> --
> http://groups.google.ru/group/sugr
> ---
> Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk
> User Group.
>
> Чтобы отказаться от подписки на эту группу и перестать получать из нее
> сообщения, отправьте электронное письмо на адрес
> [hidden email].
> Настройки подписки и доставки писем:
> https://groups.google.com/groups/opt_out.
>
>

Все верно и со всем согласен. У меня и мысли не было что Вы тут троллите.

Хочу несколько модифицировать пример:

 function append42(x: string) {

 var tmp = "42"
   if (x.length()>10) return 0;
 return x + tmp
 }

И представим что был такой вызов:

append42( append42(a) )

a - string , естественно.

Вот тут я думаю и начинается самое интересное: вдруг ни-с-того
ни-с-сего компилер начинает выдвигать
требования которые ранее не выдвигал :)
и программер в таких ситуациях обычно выпадает в осадок: все работало
и все было класно а тут я поменял одну строчку в коде и получаю 100 кг
ошибок.

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

--
Best regards,
Igor Stasenko.

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.

Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.


Reply | Threaded
Open this post in threaded view
| More
Print post
Permalink

Re: Re[2]: [RSUG] СтатичеÑ�кая типизация -- это круто?

sdfgh153

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

Я бы поспорил на тему метода проб и ошибок как самого близкого человеческому ествеству везде. Более того, я бы поспорил с противопоставлением творчества математике. На свете мало что может быть столь же творческим, как математика.
Кроме того, творчество в чистом виде это генерация случайных чисел. Творчество в том виде, который мы знаем обычно состоит из двух этапов:
  • Свободный творческий выбор (или создание) аксиоматики
  • Игра в рамках выбранной аксиоматики

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


  function append42(x: string) {

 var tmp = "42"
   if (x.length()>10) return 0;
 return x + tmp
 }

И представим что был такой вызов:

append42( append42(a) )

a - string , естественно.

Вот тут я думаю и начинается самое интересное: вдруг ни-с-того
ни-с-сего компилер начинает выдвигать
требования которые ранее не выдвигал :)

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

Намного более крутой способ вернуть "код ошибки" не ломая систему типов это multiple return values в Го и Лиспе (кусок из текущего проекта на Go):

tmpl, err := template.New("header").Parse(headerTemplate)                                          
if err != nil {                                                                                    
    panic(err)                                                                                     
}
 
Менее правильный способ: кинуть исключение. Еще менее правильный: вернуть nil-value. Но зачем делать странное? Почему при одних условиях функция будет возвращать строку, а в других, например, экземпляр битмапа с Джокондой?

и программер в таких ситуациях обычно выпадает в осадок: все работало
и все было класно а тут я поменял одну строчку в коде и получаю 100 кг
ошибок.

Первое правило программиста: читай все, что тебе пишет компилятор ;) Там же все понятно будет.

novikovs-mac:tmp nsa$ cat typetest.ts
function append42(x: string) {
    var tmp = "42"
    if (x.length > 10) {
        return 0
    }
    return x + tmp
}
novikovs-mac:tmp nsa$ tsc typetest.ts
/Users/nsa/tmp/typetest.ts(4,2): Incompatible return type
/Users/nsa/tmp/typetest.ts(6,1): Incompatible return type
novikovs-mac:tmp nsa$

--
--
http://groups.google.ru/group/sugr
---
Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group.
 
Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email].
Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out.
 
 
12