Выход mocl

Т.е. попросту «ниасилели»?

Ахаха. Во-первых, у них была задача сделать быстрый JIT, а не статический Python; во-вторых, когда язык допускает конструкции вроде:

def foo():
  fun = raw_input()
  arg = raw_input()
  return apply(fun, arg)

вполне очевидно, что полностью статически типизировать его можно только методом Харпера.

можно только методом Харпера.

Что это?

Харпер - это фамилия автора статьи по ссылке.

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

Харпер - это фамилия автора статьи по ссылке.

Я еще не дочитал.

статьи по ссылке.

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

Прочел статью, даже комментировать нечего - ни одного технического аргумента, гсм-бредня для слабоумных, пол-статьи вступление о теории заговора и как маркетологи просрали все полимеры, дальше банальный невменоз не тему в динамических языках отсутствуют типы, все untyping. Одни лозунги о «наложенном рабстве одного типа» и «динамичным быть модно», а мы суровые дебилы - модные не про нас. Приводит haskell и ml в пример, там вагон проблем с выводом типов и сами языки, особенно haskell, для анонимных марсиан, даже объектной системы нет. Ни одного блиать аргумента зато вывод «статический подход прекрасно работает». Повтрюсь - ни одного технического аргумента (о чем сам автор прекрасно понимает и о чем решил предупредить во вступлении к своему высеру). Жаль потраченного времени на прочтение. Одна хня.

Выход mocl (комментарий)

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

Подсказки вместо жестких ограничений - тоже нет?

Зачем? Оно тебе говорит о том что _однозначно работать не будет_. Зачем ты хочешь сказать «та пофик»? Чтобы писать неработающие программы?

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

Что значит «привести»? Протайпчекать? В общем случае нет. Разработка алгоритмов тайчекинга это и есть та часть которая развивается. Особенно с ограничением «открытых» программ.

Т.е., если у нас много что становится известно только в рантайме - то возможно ли это все статически типизировать?

что «это все»? Например в статически типизированной скале 2.10 есть динамическая часть. Динамическая часть это такой «тип» где можно делать что хочешь. Но это не значит что вся программа должна быть такой - это как раз и идет в область проксирования/rpc и прочего.

. Ни одного блиать аргумента зато вывод «статический подход прекрасно работает».

У тебя плохо с английским языком.

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

Ты запрещаешь или что?

Зачем? Оно тебе говорит о том что _однозначно работать не будет_. Зачем ты хочешь сказать «та пофик»? Чтобы писать неработающие программы?

За тем, что сама система сигнализирования ошибок может содержать ошибки. Или весьма неочевидные сигналы.

Что значит «привести»? Протайпчекать?

Да, но весь, а не частично.

В общем случае нет.

Почему?

Разработка алгоритмов тайчекинга это и есть та часть которая развивается.

Я рад.

Особенно с ограничением «открытых» программ.

??

что «это все»? Например в статически типизированной скале 2.10 есть динамическая часть. Динамическая часть это такой «тип» где можно делать что хочешь. Но это не значит что вся программа должна быть такой - это как раз и идет в область проксирования/rpc и прочего.

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

Ни одного блиать аргумента зато вывод «статический подход прекрасно работает».

У тебя плохо с английским языком.

ORLY? :) И отчего же ты пришел к такому мнению?

Ты запрещаешь или что?

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

За тем, что сама система сигнализирования ошибок может содержать ошибки.

И пример ты можешь привести таких ошибок в продакшен реди статических компиляторах?

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

Еще раз - если ты читал внимательно, то я хочу статический анализатор, который выполняет (но не навязывает) свои выводы об ошибках, с настраиваемым уровнем «ошибочности». Покажи мне нормальный язык с выводом типов без необходимости их декларировать *вообще*? Хаскель не катит.

За тем, что сама система сигнализирования ошибок может содержать ошибки.

И пример ты можешь привести таких ошибок в продакшен реди статических компиляторах?

java, scala (допустим) к ним не относятся. Но их система типов, и особенно необходимости их декларировать - ацкий адъ. Если бы я увидел какой-нибудь язык навроде статически типизированного лиспа или питоне - то при наличии удобных инструментов разработки для них, я бы использовал эти языки с вероятностью 99%. Тот выбор который мне сейчас предлагают статически типизированные языки - это треш и угар. А исходя из того, что представления о системе типов могут меняться, то нафейхоа мне зашитая система типов, если можно использовать внешнюю настраиваемую?

И пример ты можешь привести таких ошибок в продакшен реди статических компиляторах?

Смотря что называть продакшном.

Почему?

Открытые программы. Модульность. То что пишет тот чувак в статье.

Хотя принципиальные ограничения нужно еще доказать.

Если я зову некий мето f обекта x который транслируется в http://host/f, то на стадии компиляци a) может быть невозможно проверить если действительно такой f и b) эта проверка ничего не дает потому что на момент запуска его может и не быть. Это динамика...

ORLY? :) И отчего же ты пришел к такому мнению?

Из твоего «перевода» того что там написано:)

Хаскель не катит.

Во первых почему хаскель не катит? Во вторых ocaml. И в третьих в модульной системе с открытыми программами такое невозможно так чтобы «вообще ничего». Если у тебя есть FFI - значит его надо руками типизировать. Тут ничего не сделаешь. Если у тебя есть модульная система с раздельной компиляцией - тип может быть слишком общим, и его конкретизация может быть необходимостью, потому что сообщение о том что функция f имеет сигнатуру ...тут объединение 43 экзистенциальных структурных типов... а переда в ...35 других типов.... не всегда поможет на практике. Как буст с стлом скрещивать и материть александреску до 7мого колена.

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

ocaml, haskell.

Смотря что называть продакшном.

Это значит что это не курсовик каких-то гиков а реально используемый язык.

Я НЕГОДУЮ!!!11111

/fixed

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

Вклад в развитие Си++ Страуструпа, _автора_ языка, первого его компилятора и лучших учебников по его использованию, в развитие Си++

Учебник пересказывающий и так всем известные вещи ни разу не способствует развитию языка. «_автор_» Страуступ написал лишь несколько кривых макросов «эмулирующих» ООП и боянистое руководство.

CL Грэма, написавшего полное руководство по использованию макросов?

«Полное руководство по использованию макросов»? :) Как такое вообще может быть? Грэм писал о подходе, о МП в целом с использованием Lisp. Такой вклад конечно не сравним со Стауструповским вкладом. Вклад Грэма в разы качественнее. На его литературе основаны такие интереснейшие и хардкорные вещи, как, например, Let Over Lambda.

Признаюсь - не сразу вкурил в этот синтаксический ад, хотя код ФЯП'ов вроде ML понимаю быстро.

val bind(a, c) = map.byKeys('a,'c)

У тебя тут явное связывание идентификаторов по ключам. Т.е. вместо того, чтобы связывание производилось не явно, приходится копипастить — a, 'a; b, 'b. Также конструкция не создаёт скоуп, а просто вносит в текущий. Короче, получалась совершенно не юзабельная штука. Задача не решена.

У тебя тут явное связывание идентификаторов по ключам.

Вообще-то там нет связывания вообще.

val bind(x, y) = map.byKeys('a,'c)

Это 'совпадение':)

Также конструкция не создаёт скоуп

А зачем?

Короче, получалась совершенно не юзабельная штука. Задача не решена.

Серьезно? А ниче что на таком принципи _работает_ буквально все что движеться?

> val x :: y :: z :: Nil = List(1,2,3);
x: Int = 1
y: Int = 2
z: Int = 3

> val (ka, va) :: (kb, vb) :: (kc, vc) :: Nil = Map('a -> 1,'b -> 2, 'c -> 3).toList;
ka: Symbol = 'a
va: Int = 1
kb: Symbol = 'b
vb: Int = 2
kc: Symbol = 'c
vc: Int = 3

> val Date = """(\d\d)/(\d\d)/(\d\d\d\d)""".r
> val Date(day, month, year) = "11/01/2010"
day: String = 11
month: String = 01
year: String = 2010

и т.д.? Задача решена более чем. Никто не будет в скале такую задачу решать макрой - это чистые лиспопроблемы - в скале есть более удобные инструменты.

ocaml, haskell.

haskell - неюзабельная поделка без ооп с к месту и не к месту ленивостью. ocaml - труп с сомнительным императивным генотипом, посмотри на циклы. А от кивордов let, function, new, begin-end, class...=object, let...=new, method - к горлу подступает тошнота: одна синтаксическая избыточность, не несущая вообще никакого содержания. Веселый доступ к методам через решетку, интересно у них там есть генераторы и какой-нибудь сахарок на тему декораторов и with?

http://blog.enfranchisedmind.com/2008/05/why-ocaml-sucks/
http://www.podval.org/~sds/ocaml-sucks.html

+GIL.

Никто не будет в скале такую задачу решать макрой - это чистые лиспопроблемы - в скале есть более удобные инструменты.

Вот ты и сам признал, что макры в скале неюзбельны.

ocaml - труп с сомнительным императивным генотипом, посмотри на циклы.

Да не. Вполне обычные не ломающие ничего императивные вещи.

http://www.podval.org/~sds/ocaml-sucks.html

Мелочи. Не шибко страшно. Страшнее OCaml'овский GC и ООП, а также отсутствие вменяемого community. И да. К сожалению, OCaml — труп.

Никто не будет в скале такую задачу решать макрой - это чистые лиспопроблемы

Какие же это проблемы? В лиспе это решается макрами БЕЗ-ПРОБЛЕМ. Не нужно тащить оголтелое ФП туда, где оно не всегда нужно. На лиспе пишут как на лиспе. На скале пишут как на скале. Везде разный подход, главное чтобы бы задача решалась правильно и быстро.

Более удобного инструмента чем макры быть не может. «Инструменты» в говноскакалке - это убогая и тупая интерпретация. Макры - эффективная компиляция. Сравнивать их может только укурок с ФП головного мозга.

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

http://ncatlab.org/nlab/show/domain theory

In so-called untyped lambda calculus (whose syntax is closely connected with the theory of computability and recursive functions), all terms may be regarded as being of the same type D (which therefore need not be mentioned, hence “untyped”), so that intuitively speaking, elements of D and functions on D are treated on one and the same footing.

The problem Scott solved is to faithfully model untyped lambda calculus; in categorical terms, the basic problem is to construct a cartesian closed category with just one object D (or rather, two objects: D and a terminal object 1), so that D is closed under formation of products and function spaces: D≅D×D and D≅D⇒D. Notice that in the category of sets, the only solution is to take D≅1, so that all terms are then equal (“algorithmic inconsistency”). This is not a faithful modeling of untyped lambda calculus, which has provably unequal terms.

In 1969, Dana Scott solved this problem topologically: the terms were interpreted as continuous functions on a suitable space D isomorphic to its own function space. This D is called a domain. Decades later, we now know many techniques for constructing such domains as suitable objects in cartesian closed categories, but Scott’s basic insight, that computability could be interpreted as continuity, continues to exert a decisive influence today.

Статья 1969 года это, видимо, http://www.cs.cmu.edu/~kw/scans/scott93tcs.pdf. Ещё есть статья 1980 года, http://mathgate.info/cebrown/notes/scott80.php

Section 3. «Type-Free» Domains. The untyped lambda-calculus (without eta) can be considered as a special case of the typed lambda-calculus in the following sense. We find a domain U in a concrete CCC so that (U->U) is a retraction of U, i.e., there are maps i:(U->U)->U and j:U->(U->U) so that ji=1. Note that i is injective (so we may think of (U->U) is a subspace of U) and j is surjective (so we may think of (U->U) as a quotient space of U)--and the injection and surjection are related. We can interpret the untyped lambda-terms by converting them to typed lambda-terms interpreted in the category as follows: x*=x:U, (MN)* = j(M*)(N*), (lambda x.M)*=i(lambda x.M*). Note each M* is of type U. M=N in the type-free theory iff M*=N* in the category. Since we are assuming the CCC is concrete, U has «enough points» so that we have Rule zeta satisfied (giving weak extensionality--hence, a lambda-model). [Extensionality--the eta-rule--corresponds to the condition ij=1 giving U isomorphic to (U->U).]

Also, given a type-free theory, there is a CCC with a domain U with retract (U->U) so that the above interpretation satisfies precisely the same equations as the theory. This category is formed by taking the Karoubi envelope as in Barendregt. [There is a slight difference in the definition of products and projections.] The U is given by the identity lambda-term and the i and j are given by the lambda term 1=lambda fx.(fx) and (U->U) is also 1. Actually, every object A is a retract of U by arrows A:A->U and A:U->A. Given these definitions, it is easy to check that the interpretation of an untyped lambda term is the term itself.

Type-free domains are special kinds of types. In particular, to find a nontrivial U (i.e., U not a singleton), we must pass to an infinite type. This is already suggested in the construction of D-infinity since each D{n+1} = (Dn->Dn) is obviously a higher type than Dn, so that the limit D-infinity is an infinite type.

Not all CCC's lead to a nontrivial interpretation of the type-free lambda-calculus. For example, in Set we cannot have (U->U) a retract of U (unless U is a singleton) by Cantor's Theorem. Since all CCC's provide an interpretation of the typed lambda-calculus, we may consider the typed theory to be more general and more fundamental.

Section 5. Type-Free Domains Revisited.

...

The conclusion is that we can embed our original (typed) theory of functions into a theory containing a model of the type-free lambda-calculus given by a reflexive U. Furthermore, we can consider our original types A to be subtypes of U. Since (U->U) is a retract of U, every function f:A->B is the restriction of a function in (U->U). This is only necessarily true for the types A, B and C given in advance--not for all subtypes of U.

The untyped lambda-calculus (without eta) can be considered as a special case of the typed lambda-calculus

Since all CCC's provide an interpretation of the typed lambda-calculus, we may consider the typed theory to be more general and more fundamental.

Два хедшота тому господину :)

Давай начнём, например, с простенького: http://www.spoj.com/problems/HOMO/

И увидим один C++ в топе.

И увидим один C++ в топе.

Хотелось бы потягаться со Scala, а не с C++. Но коль уж вы настаиваете, то реквестирую решение этой задачи на С++ с использованием крестовых потоков ввода/вывода. Пишите, шлите на spoj и сорец сюда. После «победы» я сюда выложу свой сорец на sbcl.

Я там вижу только одно решение на SBCL за 5.67sec / 57M. Оно такое само по себе, или там они не дают скидку на запуск и разогрев образа? Или это не долго в данном случае? Сколько получается LOC? Какой (приблизительно) алгоритм используется?

Это 'совпадение':)

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

А зачем?

А затем, что бы связать идентификаторы со значениями и вычислить выражение с использованием значений, без лишних телодвижений и boilerplate'а. Удобно, чёрт возми.

(defmacro dict-bind (keys ht-expr &body body)
  (once-only ((ht ht-expr))
    `(let ,(loop :for key :in keys :collect `(,key (gethash ',key ,ht)))
      ,@body)))

(let ((ht (plist-hash-table '(a 1
                              b 2
                              c 3
                              d 4))))
  (reduce #'+
          (dict-bind (a b d) ht
            (list a b (1+ d))))) ; * 8

(defmacro dict-bind (keys ht-expr &body body)
  (once-only ((ht ht-expr))
    `(symbol-macrolet ,(loop
                          :for key :in keys
                          :collect `(,key (gethash ',key ,ht)))
      ,@body)))

(let ((ht (plist-hash-table '(a 1 b 2 c 3))))
  (dict-bind (a c) ht
    (incf a)
    (decf c))
  (hash-table-alist ht)) ; * ((C . 2) (B . 2) (A . 2))

Удобно, просто, быстро. Ё-моё.

Серьезно? А ниче что на таком принципи _работает_ буквально все что движеться?

Да, я на полном серьёзе. То что ты написал — лохня, которая пишется на любом языке который сколь-нибудь в малой форме поддерживает ФП и на CL такое убожество написать — раз плюнуть. Scala тут ничего нового и вечного не даёт, кроме вырвиглазного синтаксического ада. То что я написал — тоже лохня. Для Lisp. Вполне может статься, что на Scala такие вещи не написать вообще (ну или написать с болью).

Да одно — это и есть моё решение. Сорец выложу сюда, как только ты напишешь на C++ без использования сишных потоков ввода/вывода.

или там они не дают скидку на запуск и разогрев образа

Не дают.

Или это не долго в данном случае?

Долго, но что делать.

Какой (приблизительно) алгоритм используется?

Алгоритм, в целом, очевиден. Использовал одну хеш-таблицу и каунтер.

без использования сишных потоков ввода/вывода

Это обязательное условие? Может я хочу именно их использовать.

Долго, но что делать.

И на сколько процентов примерно хуже, если бы они использовали родной time?

Использовал одну хеш-таблицу и каунтер.

То есть map.

З.Ы. на скале я тоже хочу попробовать, так как там вообще на ней нет. На Java есть довольно медленные, наверно ей тоже скидок не дают.

haskell - неюзабельная поделка без ооп с к месту и не к месту ленивостью.

Какого именно ООП тебе не хватает в хаскеле?

ocaml - труп с сомнительным императивным генотипом, посмотри на циклы.

F#.

к горлу подступает тошнота:

это ты мне на фоне рубиевских @собак, def end, do end, begin rescue else end, class end рассказываешь?

Веселый доступ к методам через решетку

Какой ужос. Решетка вместо точки. Разрыв шаблона. К названию может еще претензии есть?

http://www.podval.org/~sds/ocaml-sucks.html

Спасибо - смешно.

+GIL.

Нету там никакого gil.

Вот ты и сам признал, что макры в скале неюзбельны.

Ты с дубу рухнул? Макры в скале писались чтобы решать задачи, а не чтобы перетягивать из лиспа то что в скале нахрен не впилось. Может назовем скалу неюзабельной потому что там CLOSа лисповского нету?

Какие же это проблемы? В лиспе это решается макрами БЕЗ-ПРОБЛЕМ.

Необходимость решать эту задачу. В скале все биндится как я показал.

Мусорный контейнер за углом - сходи поблюй.