Loading... |
Reply to author |
Edit post |
Move post |
Delete this post |
Delete this post and replies |
Change post date |
Print post |
Permalink |
Raw mail |
Ну я об этом и писал, что St пока сохраняет некоторое преимущество только в области среды разработки. С другой стороны очень похоже ситуация складывается с лиспом, который точно так же позволяет работать с "живой системой", однако есть довольно много статически типизированных диалектов[1] и вариантов типизации[2]. Я уже писал в чем плюсы статики, кроме того на мой взгляд снижение скорости внесения изменений на самом деле кажущееся. То есть в динамической системе вы вносите изменения и тут же получаете фидбэк, но потом-то вам все равно нужно восстанавливать непротиворечивое состояние всех частей системы, дописывать реализации новых/измененных протоколов, кастить типы и так далее. В случае со статикой этот процесс просто встает непосредственно перед фидбэком. Наверное это не всегда удобно программисту, но для продукта полезно как можно раньше узнавать о последствиях изменений. Именно для этого придумали тесты, кстати. Чтобы следить за непротиворечивостью по мере внесения изменений. Тайпчекер может взять на себя часть этих забот, добавив головняка разработчику, конечно. Но и тесты, в общем-то, создаются чтобы добавить разработчику проблем в том случае, если он что-то делает не так. Разница только в том, что типы писать сильно проще, чем тесты, которые будут проверять типы. Давайте разделим функциональные тесты, которые бытовые случаи использования статической типизации не могут заменить и тесты непротиворечивости. Некоторые глыбы академического мира могут говорить, что с зависимыми типами можно описать что угодно. Это правда, но зависимые типы пока сильно сложнее, чем написание функциональных тестов. Поэтому тесты нужно бы писать всегда, вне зависимости от типизации языка. А вот тесты непротиворечивости понятийного аппарата это как раз то, что статика закрывает прекрасно. Чтобы программист по ошибке не перепутал Божий дар с яичницей и муху с котлетой. Такие ошибки, увы, не редкость и статика тут сильно упрощает жизнь. 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]> Статическая типизация, по сути, это всего лишь специфический инструмент разработки. При этом статически типизированные языки требуют, обязывают использовать этот инструмент постоянно в процессе программирования. А что этот инструмент реально дает? Действительно ли результат работы этого инструмента повышают эффективность разработки? ... [show rest of quote] -- http://groups.google.ru/group/sugr --- Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group. Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email]. Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out. |
Loading... |
Reply to author |
Edit post |
Move post |
Delete this post |
Delete this post and replies |
Change post date |
Print post |
Permalink |
Raw mail |
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]> написал:
... [show rest of quote] -- http://groups.google.ru/group/sugr --- Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group. Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email]. Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out. |
Loading... |
Reply to author |
Edit post |
Move post |
Delete this post |
Delete this post and replies |
Change post date |
Print post |
Permalink |
Raw mail |
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. |
Loading... |
Reply to author |
Edit post |
Move post |
Delete this post |
Delete this post and replies |
Change post date |
Print post |
Permalink |
Raw mail |
> Ну не может этого быть достаточно для эффективной разработки крупной системы, для ее поддержки, для ее изучения новыми программистами (конечно, знающими язык). И в этом смысле смолтолк-подобные среды на порядок превосходят остальные технологии. Тем не менее, большинство крупных систем сегодня написано как раз не на смолтоке*. Sad but true.
Дмитрий *Java IDE относятся к смолток-подобным средам?
24 июля 2013 г., 10:27 пользователь Denis Kudriashov <[hidden email]> написал:
... [show rest of quote] -- http://groups.google.ru/group/sugr --- Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group. Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email]. Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out. |
Loading... |
Reply to author |
Edit post |
Move post |
Delete this post |
Delete this post and replies |
Change post date |
Print post |
Permalink |
Raw mail |
24 июля 2013 г., 10:34 пользователь Dmitry Matveev <[hidden email]> написал:
Нет. Но они близки в некоторых возможностях. Хотя все инструменты крайне скудны и ограничены. Например, в эклипсе вы можете выполнять код в дебагере. Но только в дебагере. И это не всегда работает. Вы можете изменить метод и продолжить. Но опять же, чаще вы получаете сообщение, что нужно остановить процесс, продолжить нельзя. Вы не можете дебажить произвольный код, нельзя запустить еще один дебагер, находясь в другом дебагере, нет инспектора в котором можно выполнять, дебажить код и открывать новые инспекторы. И если посмотреть на развитие эклипса, то средства работы с кодом они вообще не улучшают. Все что делают, это добавляют интеграцию с различными библиотеками. Кстати, Moose (проект на фаре) предоставляет различные возможности для анализа ява кода. В эклипсе такое могло бы только сниться :).
... [show rest of quote] -- -- http://groups.google.ru/group/sugr --- Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group. Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email]. Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out. |
Loading... |
Reply to author |
Edit post |
Move post |
Delete this post |
Delete this post and replies |
Change post date |
Print post |
Permalink |
Raw mail |
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]>
... [show rest of quote] -- http://groups.google.ru/group/sugr --- Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group. Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email]. Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out. |
Loading... |
Reply to author |
Edit post |
Move post |
Delete this post |
Delete this post and replies |
Change post date |
Print post |
Permalink |
Raw mail |
In reply to this post by Igor Stasenko
Так, я наверное должен извиниться за свое косноязычие и неумение донести мысль. Попробую исправить ситуацию :) Тут множество раз упоминались аннотации типов, как минус статической типизации, сведение выбора static vs. dynamic к “вкусовщине”, аппеляции к трудности вкорячивания статики в парадигму живой системы Smalltalk и много еще чего. Во всем этом виноват я, на самом деле, потому что не смог толком объяснить, что же я имею в виду, когда говорю о статически-типизированном диалекте Smalltalk. Сразу оговорюсь насчет двух вещей:
Что вообще такое статическая типизация Как выяснилось у нас уже на этом месте начинается непонимание. Для разнообразия можно почитать определение в википедии[1]:
То есть статическая типизация это таки действительно процесс, не относящийся к компиляции напрямую. Это именно статический анализ кода. Он выполняется до компиляции и основной целью этого процесса является не доказательство корректной работы логики программы, но только и только доказательство ее типобезопасности[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. Понятное дело, что для вывода типов в агрессивной для голой математики среде императивной программы, тайпчекеру нужны “зацепки”. То есть декларации типов писать все равно придется, но в разы меньше, чем можно было себе представить.
Это программа на Typescript, которая автоматически выведет тип переменной tmp и всего выражения. То есть вызвать append42(“hello”) будет можно, а вот append42(42) вызовет у компилятора неприязнь, так как он точно знает, что append42 принимает и возвращает строки, хотя у функции нет явной аннотации типа. Пример надуманный, но основную мысль передает. В Smalltalk, когда вы посылаете классу сообщение subclass: вы фактически пишете аннотацию типа. И это уже зацепка для тайпчекера. Впрочем я бы сейчас не хотел углубляться в мечтания о том, как мог бы выглядеть St со статическим выводом типов. Я глупый, пусть про это Браха думает. Резюмирую
Мне кажется все это вполне приятные вещи, которые я был бы просто счастлив увидеть в системе, “под капотом” которой находится Smalltalk с его концепцией “живой системы”, удивительным IDE и много еще чем :) Хочется еще написать о тех случаях, когда динамика действительно удобна и как такие вещи реализуются в системах со статической типизацией, но очень устали пальцы, да и литературу почитать надо. Так что в следующий раз, наверное. -- http://groups.google.ru/group/sugr --- Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group. Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email]. Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out. |
Loading... |
Reply to author |
Edit post |
Move post |
Delete this post |
Delete this post and replies |
Change post date |
Print post |
Permalink |
Raw mail |
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. |
Loading... |
Reply to author |
Edit post |
Move post |
Delete this post |
Delete this post and replies |
Change post date |
Print post |
Permalink |
Raw mail |
Скажите, а вы получили мое здоровенное письмо с пояснениями? 2013/7/31 HandleX <[hidden email]> А вот многие, говорящие про статическую типизацию, ещё имеют ввиду и последующую скорость исполнения? Т.е. у статической типизации два действующих фактора: анализ кода и последующая скорость работы в тех местах, где компилятор увидит примитивные типы, укладывающиеся в регистры процессора и станет использовать мощные низкоуровневые инструкции для работы с ними. ... [show rest of quote] -- http://groups.google.ru/group/sugr --- Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group. Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email]. Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out. |
Loading... |
Reply to author |
Edit post |
Move post |
Delete this post |
Delete this post and replies |
Change post date |
Print post |
Permalink |
Raw mail |
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. > > ... [show rest of quote] -- Best regards, Igor Stasenko. -- -- http://groups.google.ru/group/sugr --- Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group. Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email]. Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out. |
Loading... |
Reply to author |
Edit post |
Move post |
Delete this post |
Delete this post and replies |
Change post date |
Print post |
Permalink |
Raw mail |
Хоть бы крякнули что-нибудь, я же волнуюсь! Я просто писал-писал, и тут опять двадцать пять — статическая типизация и быстродействие. У меня чуть монокль от неожиданности не выпал. 2013/7/31 Igor Stasenko <[hidden email]> 2013/7/31 Semyon Novikov <[hidden email]>: ... [show rest of quote] -- http://groups.google.ru/group/sugr --- Вы получили это сообщение, поскольку подписаны на группу Russian Smalltalk User Group. Чтобы отказаться от подписки на эту группу и перестать получать из нее сообщения, отправьте электронное письмо на адрес [hidden email]. Настройки подписки и доставки писем: https://groups.google.com/groups/opt_out. |
Loading... |
Reply to author |
Edit post |
Move post |
Delete this post |
Delete this post and replies |
Change post date |
Print post |
Permalink |
Raw mail |
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. > > ... [show rest of quote] Все верно и со всем согласен. У меня и мысли не было что Вы тут троллите. Хочу несколько модифицировать пример: 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. |
Loading... |
Reply to author |
Edit post |
Move post |
Delete this post |
Delete this post and replies |
Change post date |
Print post |
Permalink |
Raw mail |
Другими словами для меня программирование это "заставить комп делать Я бы поспорил на тему метода проб и ошибок как самого близкого человеческому ествеству везде. Более того, я бы поспорил с противопоставлением творчества математике. На свете мало что может быть столь же творческим, как математика. Кроме того, творчество в чистом виде это генерация случайных чисел. Творчество в том виде, который мы знаем обычно состоит из двух этапов:
Собственно свободу творчества статическая типизация ни в коей мере не ограничивает. Вы можете сделать любую аксиоматику, вот просто "жульничать" внутри нее во время игры будет трудно. Я думаю многие писатели отдали бы почку за нечто автоматически сличающее цвет глаз у героев на протяжении всех семи томов их книги :)
... [show rest of quote] Отнюдь, он с самого начала именно такие требования и выдвигал. В этой ситуации в ошибке будет написано именно то, что и происходит: Ваша функция делает что-то не так. Почему она вдруг стала возвращать число? Компилятор просто указывает на неконсистентность и нелогичность выбранного решения. Намного более крутой способ вернуть "код ошибки" не ломая систему типов это multiple return values в Го и Лиспе (кусок из текущего проекта на Go): tmpl, err := template.New("header").Parse(headerTemplate)
if err != nil { panic(err) } Менее правильный способ: кинуть исключение. Еще менее правильный: вернуть nil-value. Но зачем делать странное? Почему при одних условиях функция будет возвращать строку, а в других, например, экземпляр битмапа с Джокондой? и программер в таких ситуациях обычно выпадает в осадок: все работало Первое правило программиста: читай все, что тебе пишет компилятор ;) Там же все понятно будет. 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. |
Free forum by Nabble | Edit this page |