это баг в SBCL или я что-то не понял?

Интересно, есть ли язык, где эта проблема решена?

Ada?

Чем больше я знакомлюсь с общелиспом, тем больше мне нравится ракет. Мне кажется, что общелисп один сплошной баг (в уж в реализации стального банка тем паче). И даже хвалёный CLOS как то не восхищает. ИМХО но объекты в ракете гораздо более зрелые в том смысле, что более современные. Макросы и вся метаязыковая парадигма вообще на порядок превосходят этот ублюдочный defmacro с мозолящими глаз gensym. Имхо но пора дать покойнику покой и сосредоточится на развитии ракетки.

Имхо но пора дать покойнику покой

Ну так дай и не лезь в темы с CL-м )))

И даже хвалёный CLOS как то не восхищает

В ракете можно использовать GLS

И даже ещё проще:

(defun BAR2 (X)
  (declare (type NUMBER X))
  (let ((Y X))
    (declare (type FIXNUM Y))
    Y))

(defun BAR3 (X)
  (declare (type (or NUMBER NULL) X))
  (let ((Y X))
    (declare (type NUMBER Y))
    Y))

Вся существенная инфа о системе типов получена из мануала по CMU CL.

Можно прибавить единицу к 2147483647 и получится -2147483648, тоже без всяких предупреждений.

Это нормально. В Си так определено сложение.

А вот про типы, кстати, аналогично:

$ cat test.c
#include <stdio.h>
int foo(char x) { return x; }
int main()
{
   int k = 300;
   printf("%i\n", foo(k));
   return 0;
}
$ gcc -Wall test.c
$ ./a.out
44

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

Её делали не для типизации, а для оптимизации компиляции. В стандарте declare вообще никаких проверок не подразумевает.

Вот и получается, если тип простой (типа fixnum или simple-array), то можно использовать быстрые операции без проверок. Если выведенный тип соответствует декларации, то можно не ставить проверку. Если выведенный тип не имеет общих значений с декларацией, значит возможно ошибка, надо кидать предупреждение.

Это нормально. В Си так определено сложение.

А в математике - не так. Я к тому, что операция + может быть определена как (function (integer-subtype-1 integer-subtype-2) bignum), а определить более точно выходной тип для двух подтипов integer-а затруднительно. И это сложение - самая простая из арифметических операций. Т.е. в Си нет целочисленной арифметики в её математическом смысле, а в лиспе хотя бы кривоватая, но есть.

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

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

Посмотрим, что напишут мне в SBCL-devel.

Её делали не для типизации, а для оптимизации компиляции.

В CL - может быть. В CMU - нет. Там написано (даже в мануале SBCL, и в CMU тоже), что при стандартной политике компиляции проверка типов точная, т.е. либо компилятор доказывает корректность, либо assert. Это отключается при safety 0. Но это не цель просто оптимизации компиляции. Это оптимизация компиляции с сохранением корректности, в т.ч. это подразумевает и выдачу предупреждений при неверных типах. В мануале CMU написано, почему так сделано. Если следовать стандарту CL и просто оптимизировать компиляцию, программа будет сегфолтиться, и это отвращает от деклараций типов. В CMU сделали костыль, добавляя assert-ы.

Интересно, есть ли язык, где эта проблема решена?

Typed Racket, Haskell

Можешь ссылку на ман для typed racket об этом?

Спасибо, погляжу.

А в математике - не так.

Так процессорная арифметика с математической мало общего имеет. Вещественное сложение даже не ассоциативно.

Я к тому, что операция + может быть определена как (function (integer-subtype-1 integer-subtype-2) bignum), а определить более точно выходной тип для двух подтипов integer-а затруднительно.

Вот для лиспового (точнее Typed Racket) +:

$ racket -I typed/racket -e "(:print-type +)"
(case->
 (-> Zero)
 (-> Number Number)
 (-> Zero Zero Zero)
 (-> Number Zero Number)
 (-> Zero Number Number)
 (-> Positive-Byte Positive-Byte Positive-Index)
 (-> Byte Byte Index)
 (-> Positive-Byte Positive-Byte Positive-Byte Positive-Index)
 (-> Byte Byte Byte Index)
 (-> Positive-Index Index Positive-Fixnum)
 (-> Index Positive-Index Positive-Fixnum)
 (-> Positive-Index Index Index Positive-Fixnum)
 (-> Index Positive-Index Index Positive-Fixnum)
 (-> Index Index Positive-Index Positive-Fixnum)
 (->* (Index Index) (Index) Nonnegative-Fixnum)
 (-> Negative-Fixnum One Nonpositive-Fixnum)
 (-> One Negative-Fixnum Nonpositive-Fixnum)
 (-> Nonpositive-Fixnum Nonnegative-Fixnum Fixnum)
 (-> Nonnegative-Fixnum Nonpositive-Fixnum Fixnum)
....
 (-> Number * Number))

Можешь ссылку на ман для typed racket об этом?

На что именно? Что арифметика лисповая или что типы проверяются статически?

Вот механизм, который позволяет в Typed Racket использовать обычные лисповые функции со статической проверкой типов:

http://docs.racket-lang.org/ts-guide/occurrence-typing.html

Давай, продолжай блистать тупостью.

eval в SBCL реализован примерно вот так:

(defun eval (code)
  (funcall (compile `(lambda () ,code))))

По теме: ты не понимаешь суть типов Common Lisp.

Начнем с того, что это не lattice, а set.

Меня интересует ситуация, когда число от 1 до 100 + число от 100 до 200 - это заведомо fixnum. Таких вот возможных теорем о типизации существует почти счётное количество (конечное, но очень большое). И для достаточно сложной функции вряд ли возможно доказать, что она не выйдет за пределы fixnum. Соответственно, возникает место или места, где нужно ставить проверки. Задача компилятора - минимизировать количество этих проверок. Хороший компилятор - тот, который ускорил тщательно подобранный микротест хотя бы процентов на 20 за счёт уменьшения проверок (а лучше - в 20 раз, но ясно, что здесь такого не стоит ждать).

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

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

(-> Byte Byte Byte Index) 

вот это ближе к делу, но это всё ещё не

(-> (integer 0 1) (integer 0 254) Byte)
...

(-> (integer 253 254) (integer 0 1) Byte)

Хотелось бы подитожить обсуждаемую тему: я хочу, чтобы лисп не разрешал мне записывать тип в более узкий тип, а требовал хотя бы явного the. Иначе это не заливная рыба.

В Typed Racket это работает, а в SBCL скорее всего придётся патчить компилятор.

Меня интересует ситуация, когда число от 1 до 100 + число от 100 до 200 - это заведомо fixnum.

Для этого нужна система типов как в Agda. Там такое статически проверяется.

Редкому мудаку все что-то ДОЛЖНЫ. Доказать, объяснить, сделать что-то за него. А он ЗАЦЕНИТ и может милостливо еще простит и поощрит. Как вы с этим долбаком на серьезе общаетесь?

Угу. Видимо, придётся патчить компилятор. Хотя сама по себе постановка вопроса «а как по-нормальному сделать числа», оказывается, тоже нетривиальная и заслуживает отдельного рассмотрения.

Вопросы «как по нормальному сделать числа» и «как по нормальному сделать строки» похоже вообще на что то довольно большое тянут. Но это так, к слову.

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

Если бы c++ согласно стандарту имел бы в рантайме весь компилятор и позволял бы себе компилить функции по-требованию он был бы интерпретируемым языком. Смех-смехом, а по факту было бы так. А g++ выступал бы интерпретатором, лол.

бред же, и вранье. вот например, в D почти так и есть. и это не делает CTFE функции интерпретируемыми.

опять же, есть libtcc например. котрый можно в рантайме дёргать. это не делает tcc интерпретатором.

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

например, CISC x86 опкоды c «логическими» РОН x86 архитектуры разбираются в RISC микрооперации и «физические» регистры

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

не обязательно. а если эта машина — времени компиляции?

вот смотри, например возьмём fasmg — абстрактный ассемблер высокого уровня, универсальный. такой метаассемблер любого ассемблера.

его метаязык:

МЕТКА: ИНСТРУКЦИЯ-ОПКОД ОПЕРАНД-КУДА, ОПЕРАНД, ЧТО, <<...>>
       МАКРОС <<..параметры..>>
       СЕКЦИИ
       ДАННЫЕ ; db, dw, dq, rb,rw, rq, dup
       ПЕРЕМЕННЫЕ времени компиляции
       ВЫРАЖЕНИЯ времени компиляции
       ; HLL-инструкции времени компиляции (тоже макросами)
       МЕТАВЫРАЖЕНИЯ (инструкции ассемблеру) времени компиляции

макросы раскрываются метавыражениями, среди которых есть iterate/irp (итератор по спискам), typeof/sizeof символ выражения времени компиляции, с символьной таблицей, match (pattern matching)

раскрываются в опкоды типа NOP в db 090h

то есть, ИНСТРУКЦИИ-ОПКОДЫ могут быть сделаны (и так и сделаны) макросами на pattern matching-е.

которые для разных платформ могут быть разными.

например, include 'x86-64.inc', include 'i8051.inc', include 'java-class.inc'

теперь, допустим макросами написан некоторый транслятор. это — метаязык времени компиляции, то есть компилятор. никакого интерпретатора тут пока нет.

например транслятор в байткод — настройка ассемблера.

набор макросов типа MasmBasic + этот бейсик времени компиляции — тоже.

или HLA, например. язык типа паскаля (а по сути, «ассемблер высокого уровня») транслируется в fasm и далее в бинарник.

никакого интерпретатора там нет.

Короче, если код не транслируется напрямую в другой код — значит он интерпретируемый.

не значит. например, autoconf — набор макросов на M4. через ./configure.sh --enable-foo --disable-bar --with-XXX -without-YYY оно специализируется в конкретный код. это не делает его «интерпретируемым».

что означает «не транслируется напрямую»? какая вообще разница сколько там слоёв метаязыков, если все они — времени компиляции?

например, вот такой код на Emacs org-mode из clojure-boot-literate : project.org в котором определена таблица project-specification в виде «блока данных», lob.org, в котором из «блока кода» в примерах lob-get-table-param достаются эти параметры из таблицы и заполняется таблица *Parameters* кодом на Elisp, определённым ниже в «блоке кода» get-table-param, get-specification-param и т.п. (boot.org и прочая)

вплоть до итогового core.org, в котором из блоков кода core/main.clj,core/main.cljs,index.html раскрываются функцией (метаязыка org-mode, на блоках кода) например get-specification-param

в конкретный helloworld (то есть, core/main.clj)

специализацией нужным параметров

времени компиляции.

когда собирается этот проект на Clojure, настроенный — все макросы раскрыты во время компиляции.

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

вот clojure-boot-literate, например — пример проекта-«остнастки», в котором текст, заданный в таблицах в «блоках кода» достаётся функциями на елиспе, собирается через org-babel-tangle в целевой файл, подставляется, параметризируется в метаязык LitProg проекта, времени компиляции и сборки этого проекта.

лисп пишет лисп.

Пара ссылок по теме:

https://news.ycombinator.com/item?id=12219304 http://www.cs.utah.edu/plt/mailarch/plt-scheme-2001/msg00803.html

http://home.pipeline.com/~hbaker1/TInference.html

Выяснилось, что компилятор SBCL работает заметно по-другому, чем CMUCL. Например, отличаются те этапы, к-рые повторяются несколько раз, см. SB-C::IR1-PHASES

В общем, совместными усилиями удалось сделать следующее: При установленном (safety 2) и установленной во время компиляции переменной sb-c::|*Запретить-неявное-сужение-типа*| , любое сужение типа внутри функции вызывает warning.

Также был сделан макрос Некое, который является аналогом the. Он отличается от the тем, что позволяет сужать тип без warning-а.

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

Никакого тестирования пока толком не было, но несколько примеров работают. Будущее покажет, что ещё нужно будет доделать.

Вряд ли вы сможете воспользоваться этим кодом без загрузки всего Яра (который давно не обновлялся и лучше живёт под офтопиком), но исходники патчей к компилятору находятся здесь:

https://bitbucket.org/budden/budden-tools/src/cc86ada29ae5e31376931742747e7d1...

А примеры - здесь: https://bitbucket.org/budden/sbcl-strict-type-check/src/d066688b71dcd1905c570...

https://bitbucket.org/budden/sbcl-strict-type-check/src/d066688b71dcd1905c570...