kouzdra - April 6th, 2013

April 6th, 2013

April 6th, 2013
11:05 am

[Link]

Еще об умножение
В эпическом треде наиболее замечательно то, что как отметил [info]38-pop@lj, народ много рассуждая о размерностях (и за и против) в массе не видит, что как раз в этом плане там формальная ошибка (причем я не уверен, что в методичке ошибка - потому как от размерностей у второклашки мозги точно в трубочку свернутся, а рассказать упрощенный, но ошибочный вариант - стандартная практика - например так теорию множеств в институте обычно рассказывают).

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

Вот по поводу типизации throw мне там чего только не писали ([info]_qwerty@lj не в счет - он просто знает ответ). Аж про "тип goto" пытались уесть (хотя в А-68 именно что goto - тоже выражение).

Вопрос о типизации throw на сам деле не пустой: потому как грязные хаки с приведениями из А-68 и С++ работают только ad hoc: например вопрос о типизации функций без результата на сам деле не пустой - а их много - failure например еще, да вообще - noreturn не даром везде в С++ естьб хоть и не входит в стандарт.

Попытки в качестве оного пристроить void тоже умилительны. Вот это как раз то решение котороне не может работать.

Работающих решения я знаю два: первое обычно для систем типов с отношением "подтип" (к коим относится С++):

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

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

Второй вариант на С++ почти пишется:
template <class T1, class T2> T1 throw (T2 exn);

Именно то, что надо - единственная проблема, что в С++ темплейты не являются типами, ну и в том, что компилятор сам не выведет тип - придется явно указывать - (b ? 1 : throw<int, Error> (e))
Но это преодолимо. А в функциональщине это просто стандартная вещь:

типы функций "без результата" - именно как правило ∀ a.a

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

Но вокруг этого кругами ходили очень долго.


*) Можно и не вводить - в принципе постулировать существование bot и top достаточно. Хотя на сам деле удобнее ввести - иначе например с типизацией того же условного выражения будут проблемы - естественный его тип "и" типов веток.

(1 comment | Leave a comment)

TimeEvent
12:10 pm

[Link]

Из комментов про методичку:
Удручает скорее то, что народ вообще не понимает какую задачу решает методичка - а решает она задачу типового способа в меру туповатому учителю (других у нас в массе нет) вложить в голову в меру туповатого второклассника представление о умножении.

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

Потому как для педагогических нужд этого достаточно, а что на самом деле там все не вполне так - ну то потом можно объяснить. Если надо будет.

(Leave a comment)

TimeEvent
06:52 pm

[Link]

9x2
Между прочим адептам коммутативности на заметку:

Возьмите в качестве примера аксиоматику Пеано (где никакой коммутативности кстати нет - там это доказывать надо) - сколько по вашему взрослых людей с высшим техническим это хотя бы знают (не говорю уж о "понимают")? Imho меньше 50%.

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

А теперь представьте себе что вы стали объяснять арифметику начиная с аксиоматики Пеано или лябмда-исчисления?

(19 comments | Leave a comment)

TimeEvent
10:49 pm

[Link]

Рефлексивное.
Я действительно в значительной степени продукт социальной инженерии - и потому видимо и не могу понять "а что тут плохого"

(Leave a comment)

Previous Day 2013/04/06
[Archive]
Next Day
My Website Powered by LJ.Rossia.org