Что круче: Лисп или Хаскелль?

Разница в том, что с $ программа напоминает нормальный юникосвый конвеер и код становится читаемее и понятнее.

> А разностные сетки, как же разностные сетки?

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

> и чем же это тебе $ не угодило? Да это, может быть, лучшее, что есть в хаскеле.

(define ($ f x) (f x))

теперь и в лиспе!

> Yeah, well, that's just, like, your opinion, man.

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

А мой самый практичный из академических (и наоборот) попрошу не трогать.

Практичный и академический - это про хаскель? Посмешили :)

> Agda и Coq — на вершине лямбда-куба, куда двигаться дальше — пока не придумали.

У лямбда куба кроме 8 вершин есть еще внутренний объем ;)

> Причём так расширяют что при использование квазицитирования ломается list comprehensive, а внутри квазицитирования не работают списки

Надежный хаскель - такой надежный.

Это если не брать во внимание, что любая монада по сути и есть маленький eDSL.

Монада - это один единственный простенький макрос. причем один на _все_ монады. понятно теперь, что подразумевают хаскиебы, когда говоря о «ДСЛ в хаскеле».

Разница в том, что с $ программа напоминает нормальный юникосвый конвеер

Не правда! Нормальный юниксовый конвеер напоминает программа с вот этим:

(define-syntax >>
  (syntax-rules ()
    [(>> x f) (f x)]
    [(>> x first f ...+) (>> (first x) f ...)]))

> Да это, может быть, лучшее, что есть в хаскеле.

Да, а закрывающаяся круглая скобка — это лучшее, что есть в CL.

А ты не тот самый дядя, который путает классы типов с полиморфными типами?

> В результате всегда могут быть выведены не те типы, что надо

Могут. С какой вероятностью? А если сравнить стоимость предполагаемых ошибок, взвешеной вероятностью этой самой вероятностью (подсказка: довольно низкой), с суммарной стоимостью потраченого времени программистов, пыхтящих над теоремами? Боюсь, картина будет не такой уж и радужной для зависимых типов.

Да, не спорю, существует ускользающе малый процент программ, (верней сказать, участков кода), цена ошибки в котором покрывает время специалиста. Для этого участка можно и теорем в той же Изабелле накатать, и в тот же Хаскель сгенерировать. Для всего остального — вроде должно быть понятно.

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

>> что займет лишние байты и такты

occurence typing же! чекер выведет типы на основе кода и элиминирует лишние проверки.

лишние проверки это еще не все, меня интересует именно чтобы тайптег был полностью optimized out

собственно это и будет означать статическую типизацию :-)

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

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

2. все вызовы f(a,b,c,d) при условии, что все аргументы могут быть вычислены в компайл-тайме, вычисляются; среди аргументов могут быть тайптеги или их так сказать части (это те самые вычисления на типах)

> с суммарной стоимостью потраченого времени программистов, пыхтящих над теоремами?

Над какими теоремами? Мы о выводе типов, а не о тайпчеке говорили. При чем тут зависимые типы-то?

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

Все дело исключительно в отсутствии развитых средств статической отладки. Когда такие средства появятся? специалисты будут не нужны - нанял 10 студентов за доширак и они тебе все докажут.

Верно, скобки --- это лучше, что есть в лиспе. "(" --- α и "(" --- ω. Начало и конец.

> лишние проверки это еще не все, меня интересует именно чтобы тайптег был полностью optimized out

Зачем нужен язык, в которой тайптег полностью optimized out? Это же получится убогое говно, не способное ни к какой интроспекции. Спасибо, не надо такого счастья.

2. все вызовы f(a,b,c,d) при условии, что все аргументы могут быть вычислены в компайл-тайме, вычисляются;

Ну это простейшая оптимизация, в том же лиспе несложно написать небольшой макрос, который вычислит 95% подобных вызовов.

>> В результате всегда могут быть выведены не те типы, что надо

Могут. С какой вероятностью?

с высокой

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

я уж тут на лоре писал, что вывести unsigned в account.send_money_to(Account receiver, unsigned int money) нереально и катастрофически ненадежно

> Зачем нужен язык, в которой тайптег полностью optimized out? Это же получится убогое говно, не способное ни к какой интроспекции. Спасибо, не надо такого счастья.

бугага

статическая типизация это именно возможности интроспекции без тайптега *в данных*

> статическая типизация это именно возможности интроспекции без тайптега *в данных*

Так смысл интроспекции именно в том, что вывести типы в компайлтайме просто нельзя :)

> Так смысл интроспекции именно в том, что вывести типы в компайлтайме просто нельзя

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

>>> В результате всегда могут быть выведены не те типы, что надо

Могут. С какой вероятностью?

с высокой

Секундочку, мне кажется, что ты не уловил контекст. Я говорю о вероятности того, что при не указаном типе и неверном коде тайпчекер Хаскеля выведет неверный тип и проверка типов пройдёт успешно. В моей практике такого не было ни разу.

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

Т. е. фактически, тесты? Их-то ведь никто не отменял ещё.

в общем, анонимус, твою идею можно модернизировать до вполне приемлемой юзерами статической типизации (хотя, что интересно, похоже тебе эта модернизация не нравится)

> Т. е. фактически, тесты? Их-то ведь никто не отменял ещё.

*предикаты*, епрст, а не тесты

Я говорю о вероятности того, что при не указаном типе и неверном коде тайпчекер Хаскеля выведет неверный тип и проверка типов пройдёт успешно. В моей практике такого не было ни разу.

«№;% !

account.send_money_to(Account receiver, unsigned int money)

> Над какими теоремами? Мы о выводе типов, а не о тайпчеке говорили. При чем тут зависимые типы-то?

При том, что мы говорили о том,

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

А также о том, что dependent types, в отличии от, перспективное направление.

Все дело исключительно в отсутствии развитых средств статической отладки. Когда такие средства появятся? специалисты будут не нужны - нанял 10 студентов за доширак и они тебе все докажут.

Свежо преданьице.

> Секундочку, мне кажется, что ты не уловил контекст. Я говорю о вероятности того, что при не указаном типе и неверном коде тайпчекер Хаскеля выведет неверный тип и проверка типов пройдёт успешно. В моей практике такого не было ни разу.

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

>Бред. «Научные круги» на 99.9% состоят из тех кому нужны численные методы, формулируемые в терминах императивных языков. Из этих «99.9» чуть меньше чем все используют готовые продукты, специализированные в конкретной области. «Научные круги», как ты выразился, больше волнует погрешность разностной схемы чем мнения ЛОРовских языковедов.

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

>еще внутренний объем

Ыыы? Он же дискретный!

> статическая типизация это именно возможности интроспекции без тайптега *в данных*

И каким образом?

Я говорю о вероятности того, что при не указаном типе и неверном коде тайпчекер Хаскеля выведет неверный тип и проверка типов пройдёт успешно. В моей практике такого не было ни разу.

ладно, рассмотрим именно хаскель

пусть у нас имеется все тот же account.send_money_to(receiver, money_to_send)  — сорри за императивный синтаксис — и программист неверно написал что-то вроде

account.money  -= money_to_send;
receiver.money += money_to_send;

account.money -= 0.01*money_to_send;
bank.money    += 0.01*money_to_send;

тогда все тайпчекнется и тип денег окажется все что угодно, но не Integral, не?

> в общем, анонимус, твою идею можно модернизировать до вполне приемлемой юзерами статической типизации (хотя, что интересно, похоже тебе эта модернизация не нравится)

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

> *предикаты*, епрст, а не тесты

типы = предикаты - это как раз в сторону occurence typing тебе :)

>> статическая типизация это именно возможности интроспекции без тайптега *в данных*

И каким образом?

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

> Ыыы? Он же дискретный!

Я какбе имел в виду, что есть огромное количество систем с интересными свойствами, которых в лямбда-кубе нет. Ну логично взять и поместить их куда-нибудь внутрь кубика, например :)

> тогда все тайпчекнется и тип денег окажется все что угодно

Нет, так не получится. При объявлении структуры необходимо указывать типы полей, и тип денег (целочисленный, надо полагать) будет закреплён именно там.

>>> статическая типизация это именно возможности интроспекции без тайптега *в данных*

И каким образом?

когда доказано, что здесь могут быть только данные вполне определенного типа

Да где «здесь»? Вот есть процедура, печатающая имя типа переданного ей значения. Как ты тут без тайптега?

> При том, что мы говорили о том,

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

Свежо преданьице.

Ну вообще-то свежо, да. Это как раз то самое перспективное направление, которым не занимаются :)

> Нет, так не получится. При объявлении структуры необходимо указывать типы полей, и тип денег (целочисленный, надо полагать) будет закреплён именно там.

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

> Ну логично взять и поместить их куда-нибудь внутрь кубика, например :)

Почему не снаружи?

>> Нет, так не получится. При объявлении структуры необходимо указывать типы полей, и тип денег (целочисленный, надо полагать) будет закреплён именно там.

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

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

> Да где «здесь»? Вот есть процедура, печатающая имя типа переданного ей значения. Как ты тут без тайптега?

похоже ты не понял что я говорил, и я не знаю, помогут ли понять ответы на твои вопросы

исходи из того, что я знаю, что в общем случае без vtbl обойтись нельзя

впрочем, можем продолжить...

откуда вызывается эта процедура? из отладчика или из компилируемого исходного кода?

>> При том, что мы говорили о том,

А, ну да. Дело тут вот в чем - вывод типов сама по себе штука вредная, а еще и ограничения на систему типов налагает. Плюсов же от него - никаких нет. Вот и вопрос - нафига оно?

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

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

Может быть, но хотелось бы ссылочек на авторитетные источники.

> типы = предикаты - это как раз в сторону occurence typing тебе :)

понятно, что из исходников надо уметь по-максимуму высосать предикатов, но все равно этого будет недостаточно — придется их ставить ручками, и много

> исходи из того, что я знаю, что в общем случае без vtbl обойтись нельзя

Интроспекция - это как раз тот общий случай.

Ну а новые идеи где?

Что ты понимаешь под словом «новое», анон?

но вместо того, чтобы развивать dependent types, занимаются высасыванием из пальца и обжовыванием всякой тривиальщины

Да ну?

во всякой покрытой пылью времен бестолковщине типа GADT.

А. Я понял. Тебе, видимо, лет десять, и в твоём возрасте время воспринимается иначе. Пройдёт.

никаких проблем: [code] (cond [(vector? v) ...] [(normalized-vector? v) ...]) [/code]

Ага, только это не компайл-тайм, а рантайм. Не пойдёт.

Иначе вместо того, чтобы выводить типы, тайпчекер сам начнёт требовать доказательств.

Тут, кстати, некая тонкость имеется, да. Зависимые типы много позволяют, но много и требуют – по крайней мере, пока. Не будь вывода типов, я бы сказал, что и статическая типизация, в основном, вредна. Он, к счастью, есть.

Что круче: Лисп или Хаскелль?

Чак Норрис. А при чём тут лисп и хаскель я так и не понял.

Фу-у-у. Прямая работа со стеком и язык высокого уровня – вещи, ИМХО, вообще несовместные.

Я ожидаю от компьютера решения тех задач, которые сейчас решаю я.

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

>> исходи из того, что я знаю, что в общем случае без vtbl обойтись нельзя

Интроспекция - это как раз тот общий случай.

мне ничего не остается, как повторить — в тех частных случаях, когда без тайптега можно обойтись, 1. без него необходимо обходиться, 2. интроспекции это не мешает, и 3. похоже, только в этих случаях и можно говорить о статической типизации

Причём так расширяют что при использование квазицитирования ломается list comprehensive, а внутри квазицитирования не работают списки

Но ломает что-то, как я понимаю, только квазицитирование. Которое, вроде как, last resort. Остальные расширения внедряются в синтаксис незначительно, ничего не нарушая.

> Ну это уже какой-то другой язык программирования, не Хаскель.

Ну почему же? Может быть и в хаскеле: let f x y = x + y f 2 2.0 все корректно чекается а должен быть эррор

И как такое возможно, что операция, определённая на широком типе, неприменима к узкому?

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

Практичный и академический - это про хаскель?

Разумеется. Язык весьма практичен, если забыть про эту ересь со стеком.

Дело в том, что алгоритма вывода типов, который бы выводил типы, ожидаемые программистом, пока не существует.

Естественно, и не может быть. Может, программист сумасшедший?

Другое дело, что алгоритм вывода типов устанавливает, может ли данное выражение ВООБЩЕ быть типизировано. И это оччень сильная проверка.