Ололо.

Дошел до этого места и перестал читать

А зря, там же дальше написано.

Именно тут появляется равенство по определению, definitional equality.
термы mul 2 9, mul 9 2 и fst (18, 'x') равны по определению

Ты не знаешь, что такое применение функции. Это просто замена всех вхождений аргумента на его значение. Т.е. это просто какая-то манипуляция со строкой символов. Если mul:Nat->Nat->Nat это функция, или, проще mul x y. Подставляем вместо x 9, вместо y 2 и получаем... mul 9 2. По определению, (mul 9 2):Nat.

Все что Вы написали на рабоче-крестьянском языке означает, что тип в хаскеле это-некий класс объектов и операций над этими объектами. Это голимый ООП, разукрашенный «модными словечками»

тип в хаскеле это-некий класс объектов и операций над этими объектами

Нет, лол. И причем тут хасклеь вообще? Мы говорили о теории типов.

на рабоче-крестьянском языке

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

Нет, лол.

Можно на пальцах, в чем отличие.

И причем тут хасклеь вообще

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

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

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

А mul(9):Nat->Nat. Сказать то ты чего хотел? Там выше ссылка с рассуждением категориста о равенстве 2*9 и 9*2, где он заявляет что операция mul входит в тип Nat. Так вот я и хотел поинтересоваться, что такое тип?

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

Сказать то ты чего хотел? ... он заявляет что операция mul входит в тип Nat.

Хотел то, что сказал. Там этого нет. mul входит в тип Nat->Nat->Nat. А вот результат ее применения к 2 и 9, т.е. _выражение_ mul 2 9 входит в тип Nat. Где ты тут увидел утверждение, что функция в ходит в тип Nat?

что такое тип?

Это сложный вопрос.

Чувак неверно понимает, что такое тип. А аналогия между типами (классами типов) в хашкеле и классами и шаблонными классами в си++ действительно есть. Не буду распространятся, т.к. не знаю хаскель.

Я вообще не понимаю, зачем ты влез в спор со своим хаскелом. Речь шла о теории типов и основаниях математики (в этом подтреде).

Не надо только стыдливо делать вид, что эти 2 темы никак не связаны. Одно отображается в другое.

о теории типов и основаниях математики

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

Конечно связаны. Ты бы мог еще вспомнить теорию категорий, мамкин борщ etc. Только причем тут это?

Не буду распространятся, т.к. не знаю хаскель.

Я это понимаю не зная ни то ни другое. Много ума не надо, чтобы это понять.

Только причем тут это

Как это причем? Мы в разделе Development, как-никак. Да и вообще такие вещи легче усваиваются когда разбираются на реальных примерах.

Кроме того, меня очень интересует сейчас тема деградаци математики и програмирования, иными словами, как мы (человечество), докатились до хаскеля и теории типов.

Формально есть разница, работаешь ты в ZFC или type theory или где-то еще. Хотя математики забивают на это, конечно.

Там этого нет.

оу, пардон, действительно нет.

Хотел то, что сказал. Там этого нет. mul входит в тип Nat->Nat->Nat. А вот результат ее применения к 2 и 9, т.е. _выражение_ mul 2 9 входит в тип Nat. Где ты тут увидел утверждение, что функция в ходит в тип Nat?
Т.е. терм mul 9 2 - полноправный элемент типа Nat. Не число в привычной нам форме, не результат вычисления функции mul, а само выражение
А вот результат ее применения к 2 и 9
не результат вычисления функции mul

Кому из вас верить поцаны?

Ему вестимо, он больше шарит в данном вопросе.

деградаци математики и програмирования

Что, лол? Это не деградация, это прогресс. Чем сильнее абстрагируемся от машины, тем все становится проще.

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

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

Может то что он там пишет - это что-то вроде как математики обычно пишут: 3*<корень из n>, абстрагируясь, как-бы, что корень еще не вычислен? Получается, числа, разных типов, но насрать, потом, дескать, посчитаем на калькуляторе, а теперь это «узаконили»:

Получается, числа, разных типов, но насрать, потом, дескать, посчитаем на калькуляторе, а теперь это «узаконили»:

это «теперь» узаконили ещё черт его знает когда и впихнули в лямбда-счисление (подправьте меня, если не прав, я в этом понимаю чуть менее чем нифига)

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

Чем сильнее абстрагируемся от машины, тем все становится проще.

Если серьезно, и не приминительно к машине, а к абстракции вообще, то по моим наблюдениям типы как-раз таки ограничивают абстракцию. В естественном языке мы можем применить к примеру, слово ху..ня, к очень широкому классу объектов и явлений, а если бы нас ограничили типами, мы могли бы применить его только к в контексте гениталий. Пришлось бы «произносить монады», например: «случилась эта ху..ня, но я имею в виду эта ху..ня в таком то контексте смысле, а не в смысле генитальной темы ...», Хотели бы вы разговаривать на таком языке? А придется...

Ну, пиши сразу в маш коде. Принципиальной разницы для процессора нет.

Хватит чушь писать.

ты там песню ищёшь

опознать песню

основная мелодия - это припев «Eminem - Sing for the moment»

Все языки статически типизированные: http://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-...

весь шум статическая vs динамическая яйцавыеденного не стоит

Смелое заключение для нуба в программировании.

Ну ты открыл америку.

Я не претендовал на открытие.