Типы и типы

[metaclass]

Очевидно ли, почему flatten и (partial apply concat) в Clojure могут выдать разные результаты? После хаскеля кложурный flatten, работающий на все уровни "вглубь", выглядит непривычно.

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

Comments

[djuffin.livejournal.com]

Все верно, с такой типизацией, возможность совершить ошибку совершенно исключена.

[trueblacker.livejournal.com]

по-моему, это как минимум фраза дня. А то и более.

[kkirsanov.livejournal.com]

--По ходу, статическая типизация делает невозможными некоторые типы программ, возможные при динамической.

Нет, просто приходится вручную описывать все варианты, что в динамике даются на халяву. Таким образом, функция объема статического кода от динамического, - как минимум, степенная.

Путем наворачивания крутых статических типов можно довести объем статического кода до динамического.

Т.е. в пределе крутой статический код это простой динамический.

[thesz.livejournal.com]

>функция объема статического кода от динамического, - как минимум, степенная.

Функция стоимости же...

[theiced.livejournal.com]

ты от мамочки уже съехал?

[migmit.livejournal.com]

Осторожно, он может знать, где ты живёшь.

[metaclass.livejournal.com]

Ай, сильно далеко ехать )

[migmit.livejournal.com]

Разве ж это крюк.

[cp-poster.livejournal.com]

> По ходу, статическая типизация делает невозможными некоторые типы программ, возможные при динамической.
Это тянет на теорему. Какие например типы?

[thesz.livejournal.com]

Вот именно.

И к заявлениям metaclass: зависимые типы делают большее количество программ допустимыми.

[metaclass.livejournal.com]

Мы тут с theiced на эту тему спорили. Он привел пример вроде

charAt s i = s.[i]

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

[thesz.livejournal.com]

Это же на Хаскеле даже можно сделать.

Кстати, пример с корректной адресацией элементов массива идёт не то первым, не то вторым примером в какой-то из статей про Эпиграм. Вот трансляция оттуда в Хаскель по памяти:

{-# LANGUAGE GADTs #-}

data Zero = Zero
data Succ n = Succ n

data Vec len a where
	Nil :: Vec Zero a
	Con :: a -> Vec len a -> Vec (Succ len) a

data NatUp up where
	Z :: NatUp (Succ len)
	S :: NatUp len -> NatUp (Succ len)

charAt :: Vec len Char -> NatUp len -> Char
charAt (Con c _) Z = c
charAt (Con _ v) (S n) = charAt v n

good = charAt (Con 'a' Nil) Z
--bad = charAt (Con 'a' Nil) (S Z) -- не пройдёт!!!

[metaclass.livejournal.com]

О.
Т.е. если мы вводим s пользователем, то полный тип программы выведется только после ввода строки, или не выведется, потому что пользователь ввел "a" а мы обращаемся ко второму символу.
Соответственно, вместо обработки исключений в рантайме у нас вывод типов в рантайме, причем нужно еще куда-то сунуть локализуемое сообщение об ошибке, чтобы его показать пользователю.

Это можно сделать на зависимых типах?

[thesz.livejournal.com]

>Т.е. если мы вводим s пользователем, то полный тип программы выведется только после ввода строки, или не выведется, потому что пользователь ввел "a" а мы обращаемся ко второму символу.

Нет.

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

Гарантии указаны в типе. Контракте, если изволите.

Нарушение контракта можно переводить в сообщение об ошибке.

[metaclass.livejournal.com]

А, пользователю просто нельзя дать ввести строку, короче, чем мы к ней обращаемся. Мы ее просто никак не скастуем к допустимому для системы типу.

[thesz.livejournal.com]

Именно так.

[si14.livejournal.com]

Посмотрите http://www.bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.html , там достаточно пространно объясняется, что такое зависимые типы и что на них можно сделать.

[zmila.livejournal.com]

а в pascal

type
  my_range = 1 .. 21;
  my_string = array [my_range] of char;
var
  my_i : my_range;
  my_s : my_string;

не то?

[thedeemon.livejournal.com]

Я показывал примеры, как на языке с упрощенными зависимыми типами это легко делается
http://thedeemon.livejournal.com/41035.html

[metaclass.livejournal.com]

Тут в комментариях поправили: сделать то же самое на статике можно, но в те места, где я сейчас передаю просто хеш-мап-словарь-объект с несколькими вариациями полей, придется засовывать либо алгебраический тип с возможными вариантами, если их конечное количество, либо экзистенциалы, с тайпклассами типа "меня можно использовать как параметры запроса" и "меня можно сохранить в json"

А когда дело доходит до того, что кроме json нужно отдать еще и html/xml/csv как положено RESTful сервису, сигнатуры типов начинают рыдать кровавыми слезами.

[thesz.livejournal.com]

В Хаскеле и многих других ЯП есть строго типизированный Dynamic.

И типы в порядке, и динамичность есть.

[thedeemon.livejournal.com]

В ОО-языках это делают интерфейсами, значит в хаскелях делается тайпклассами, навороченные АДТ тут не нужны.

[(Anonymous)]

а вот вопрос можно?

имхо основное практическое удовольствие хаскеля в алгебраических типах данных, и с ними можно наводить порядок в запутанной логике и куче таблиц в бд, да?
ну или там веб-сервисы какие-нибудь, которые всё время меняются.
когда целая куча разных чужих сервисов, которые меняют как попало совершенно левые люди, удовольствие делать э.. интеграционную программу уменьшается (

как отражать в статических типах данных эти изменения?

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

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

[metaclass.livejournal.com]

Вот в этом основная проблема и оказалась.
Требуется вывод типов не "во время компиляции", а "при запуске программы" или "при проверке не изменилась ли схема внешнего источника данных".

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

[thesz.livejournal.com]

Некоторые Хаскельные библиотеки связи с БД поддерживают миграцию.

[metaclass.livejournal.com]

Лучше бы их вообще не было :)
Большая часть ORM и тому подобного на любых языках - тяжкий невыносимый ад.

[(Anonymous)]

может я ща фигню сморожу, но просто пока в треде много хаскелистов, можно попробовать:

а имеет смысл как-нибудь привязать к каждому типу данных номер коммита или текущую дату, а потом делать линк с коротких обычных имён типов данных на самые последние по времени?

и описать миграции (в какую получится сторону в каждом случае).

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

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

может правда это нихрена хорошего и не даёт, я хз (

[victor bolshakov (from livejournal.com)]

А чем существенно компиляция от запуска отличается? Ну кроме того как оно сейчас реализованно...

[metaclass.livejournal.com]

В кложури вообще ничем.

[(Anonymous)]

а ещё грят у злодеев из эрланга есть демоническая перезагрузка кода (нахаляву), и вообще они якобы с самого начала стараются строить программу так, чтобы она после этой перезагрузки не только падала, но и поднималась обратно ((
c:Conner, whysmai

[theiced.livejournal.com]

в кложуре можно вообще сванк в прогу всунуть и говнокодить прям в работающем продакшне.

[(Anonymous)]

тебе смешно, а как в руби такую хрень замутить.. (
тока не надо писать, что это не нужно.
там вон у народа была какая-то zeromq, но хз как это поможет (

[blackyblack.livejournal.com]

Есть такая. Штука действительно демоническая, но в целом понятная. Там просто супер-цикл, в котором постоянно обрабатываются сообщения. Можно залить код, положить его рядом, а потом послать сообщение, в котором выполнение перенаправится на новый код. Такую штуку можно сделать и в обычных языках, но за счёт ориентированности на обработку сообщений и функциональный стиль, получается просто и из коробки такой трюк.

[kurilka.livejournal.com]

Не надо там сообщений, просто следующий вызов module:function(...) после обновления приведёт к выполнению кода уже нового модуля (за минусом подробностей типа gen_server:conde_change/3 и т.п.)

[blackyblack.livejournal.com]

Не верю. Насколько я помню, в книжке явно слали сообщение для замены кода.

[kurilka.livejournal.com]

Ну против верований возражения придумывать нет желания.
Реально же достаточно в консоли l(module) сделать, но по-нормальному, конечно, стоит release_handler использовать, а в принципе в документации все описано - http://www.erlang.org/doc/man/code.html#id101126

[blackyblack.livejournal.com]

code:load_file я делал. Но, насколько я помню, если в модуле рекурсивный вызов без обработки сообщений, то обновить такую функцию нельзя.

[kurilka.livejournal.com]

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

[blackyblack.livejournal.com]

Вперед, за нобелевкой. За доказательство существования "некоторых невозможных типов программ".