А вот скажите, господа.
То, что здесь удаляют все сообщения с критикой Nemerle как декларативного языка — это как, официальная политика заведения или полуофициальная?
Мне правда хотелось бы это знать, потому что мне неприятно, когда я сначала трачу свое время на то, чтобы мотивированно объяснить какие-то вещи, а потом обнаруживаю, что от моих сообщений не осталось и следа.

Здравствуйте, Аноним, Вы писали:

А>То, что здесь удаляют все сообщения с критикой Nemerle как декларативного языка — это как, официальная политика заведения или полуофициальная?

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

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

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

Никаких объяснений, тем более мотивированных я не обнаружил. Надеюсь модератор руководствовался той же логикой, что и я. Да и твое новое сообщение тоже не имеет никакого отношения к тематике форума, обычно жалуются на жизнь в форуме "Обсуждение сайта". Думаю что стоит перенести эту тему туда.

<Аноним>,

А>А вот скажите, господа.
А>То, что здесь удаляют все сообщения с критикой Nemerle как декларативного языка — это как, официальная политика заведения или полуофициальная?
А>Мне правда хотелось бы это знать, потому что мне неприятно, когда я сначала трачу свое время на то, чтобы мотивированно объяснить какие-то вещи, а потом обнаруживаю, что от моих сообщений не осталось и следа.

Может вместе с критикой Немерле ты заодно проехался и по участникам форума?

Что же касается самого языка Немерле как языка программирования, то он будет обладать теми фичами, которыми он обладает и позволять такие языковые конструкции которые он позволяет независимо от того, какой ярлык к нему прилепят конкретные сторонники/противники — "декларативный" ли, " императивный" ли, "похожий на Схему", "непохожий ни на что" и так далее. Язык останется языком, это объективная реальность.

Декларативный, императивный, функциональный, логический — это всё термины с размытыми границами. Чтобы показать, что Немерле не декларативный, нужно чётко определить что такое "декларативный". Предлагаешь спор о терминах? (Был уже недавно "дзен-дубизм", по-моему хватило всем).

Здравствуйте, Lazy Cjow Rhrr, Вы писали:


LCR>Может вместе с критикой Немерле ты заодно проехался и по участникам форума?

Ни по каким участникам я не проезжался, что за инсинуации вообще?

LCR>Декларативный, императивный, функциональный, логический — это всё термины с размытыми границами. Чтобы показать, что Немерле не декларативный, нужно чётко определить что такое "декларативный". Предлагаешь спор о терминах?

В математике что, так часто бывают терминологические споры? Первый раз слышу.

Декларативный четко определяем.
Декларативный язык = формальная система

equational logic, rewrite logic, rho calculus, first order predicate calculus, lambda calculus, SKI combinator calculus, Girard's System F и всяческие производные — это декларативные языки.

Nemerle таковым не является по причине отсутствия явно и формально определенных аксиом и правил вывода.
Иначе о какой вообще декларативности можно говорить, если даже невозможно в его рамках определить понятие "декларации".

Именно это я и написал в удаленных сообщениях. Подозреваю, правда, что и это удалят вслед за ними.

Здравствуйте, Vermicious Knid, Вы писали:

VK>Я конечно не модератор и не мне решать, но честно говоря не увидел в твоих сообщениях никакой критики Nemerle. Да и вообще сложно что-то критиковать без знания предмета. Как показывает опыт пожалуй здесь мало кто сможет достойно критиковать Nemerle.

Да ради бога, не увидели — и прекрасно. Разумеется, ни у кого вообще ни ума не фантазии не хватит, чтобы суметь раскритиковать хоть одну слезинку Nemerle.

VK>Честно говоря я могу привести десятки претензий к дизайну Nemerle, в том числе к декларативной его составляющей.

Декларативная составляющая — это оксиморон, это бессмысленное понятие, но, впрочем, у вас, кажется, были претензии и к предикатному исчислению (в удаленных сообщениях).

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

Все, о чем я сказал — это что Nemerle не декларативный язык. Не более, чем C++, ruby или Visual Basic.
И почему вам лично хочется считать его таковым, я тоже не понял (ничего кроме возгласов "на себя посмотри" и "разберись в предмете" я не услышал).

Здравствуйте, <Аноним>, Вы писали:

А>А вот скажите, господа.
А>То, что здесь удаляют все сообщения с критикой Nemerle как декларативного языка — это как, официальная политика заведения или полуофициальная?

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

Лично я ничего не удалял вроде. Модераторы вообще не удаляют мнения даже если они делетанские.
Удаляются обычно сообщения несущие оскорбления, кливету на людей, мат и другие ругательства.

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

Что касается твоего времени, то потратил бы лучше его на изучение критикуемого вопроса. Может тогда и критиковать то нечего было. А то тот декларативные конструкции Немерла слизаны чуть ли не 1:1 с ML-подобных языков. А они в свою очередь являются классикой диекларативных языков.

Здравствуйте, Vermicious Knid, Вы писали:

VK>Честно говоря я могу привести десятки претензий к дизайну Nemerle, в том числе к декларативной его составляющей.

Кстати, приоводи. Конструктивная критика и ее анализ (читай критика критики ) всегда полезны. К тому же Немрле не закрытый язык. В нем можно многое еще изменить.

Лично я добился изменение пары вещей которые мне не нравятся (например, отмены неявного приведения void к object).

VK> Но кроме того, что у ненавистников Nemerle появится шанс позлорадствовать, это будет абсолютно бесполезной тратой времени.

Не скажи. Это интересно очень многим.
А то что у языка уже есть ненависники, да к тому же незнающие язык толком — это очень хорошо. Это говорит, о том, что язык будет жить. А это пожалуй самое главное!

VK> Проще всего оформить претензии непосредственно разработчикам языка и выслушать их аргументацию, возможно дав им пищу для размышлений по улучшению языка. Таким образом в Nemerle кстати зачастую и делаются улучшения, это достаточно быстро развивающийся проект и user feedback играет в его развитии не последнюю роль.

+1

VK>Никаких объяснений, тем более мотивированных я не обнаружил. Надеюсь модератор руководствовался той же логикой, что и я. Да и твое новое сообщение тоже не имеет никакого отношения к тематике форума, обычно жалуются на жизнь в форуме "Обсуждение сайта". Думаю что стоит перенести эту тему туда.

Ну, дадим товарищу возможность высказаться. Если он не перейдет к делу, т.е. к критике языка, то снесем.

Здравствуйте, <Аноним>, Вы писали:

А>Декларативная составляющая — это оксиморон,

На мой взгляд, довольно неразумное утверждение.

А>Все, о чем я сказал — это что Nemerle не декларативный язык.

А кто-то спорил? Nemerle — гибридный язык! В нем есть декларативные конструкции взятые из ФЯ, есть макросы — средство создания декларативных конструкций которых нет в языке, и есть ООП, императивщина, обобщенное программирование (ака параметрический полиморфизм) и т.п.

Так что тут с тобой почти все будут согласны. Nemerle не является ни Pure ФЯ, ни Pure ООП. Это гибрид. Удачный на мой взгляд, и на взгляд многих других ледей.

А> Не более, чем C++, ruby или Visual Basic.

Пожалуй на счет Руби я соглашусь. Руби тоже гибрид. И тоже довольно удачный. Но у него другая ниша. Это скриптовый язык и этим все сказано.

Что касается Visual Basic — это это чисто императивный ОО-язык. Так что на сравление с Nemerle он не катит. C++ имеет мощьную, хотя и очень переусложненную подсистему обобщенного программирования, как ООЯ он тоже весьма неплох, но вот в области метапрограммирования и темболее в области поддержки функциональной парадигмы он проигрывает Nemerle в чистую.

Скорее всего самый близкий язык к Nemerle — это OCaml, как не странно.
Думаю, тебя эта мысль сильно озлобит, но это так. Очень уж многое Nemerle позаимствовал из ML. К тому же OCaml как и Nemerle поддерживает ООП.
Основная разница в языках это синтаксис вызова метода и подстистема вывода типов. Последнее вооще являяется ноухау языка. Эта система преспособлена для синтаксиса а-ля "С", но позволяет при этом производить вывод типов и не вызвает проблем в выявлении ошибок.

А>И почему вам лично хочется считать его таковым, я тоже не понял (ничего кроме возгласов "на себя посмотри" и "разберись в предмете" я не услышал).

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

Если это будет так, то мы с удовольствием обсудим с тобой все твои мысли и возможно даже согласимся с ними.

Здравствуйте, Vermicious Knid, Вы писали:

Где вы с ним дискутировали то? Дай, плиз, ссылочку.

Здравствуйте, VladD2, Вы писали:


VD>Скорее всего самый близкий язык к Nemerle — это OCaml, как не странно.

Окамл — это типизированное по Карри-Говарду лямбда-исчисление с аппликативной редукцией
Какой декларативный формализм лежит в основе Nemerle?

Здравствуйте, VladD2, Вы писали:

VD>Что касается твоего времени, то потратил бы лучше его на изучение критикуемого вопроса. Может тогда и критиковать то нечего было. А то тот декларативные конструкции Немерла слизаны чуть ли не 1:1 с ML-подобных языков. А они в свою очередь являются классикой диекларативных языков.

Спасибо, я уже потратил на изучение этого вопроса 10 лет.
Ничего у Nemerle с ML не слизано, ни одной аксиомы. Не считать же таковой аппликативность.

Здравствуйте, Аноним, Вы писали:

А>Спасибо, я уже потратил на изучение этого вопроса 10 лет.

Главное вовремя остановиться. А то станешь как ученый с мировым именем Иннокентий.

Здравствуйте, Аноним, Вы писали:

А>Окамл — это типизированное по Карри-Говарду лямбда-исчисление с аппликативной редукцией

Да все то же типизированное лямбда-исчисление. Самое главное различие Nemerle и Ocaml это система типов. Императивные конструкции в языке(а все они реализованы макросами), если копнуть все равно раскрываются в функциональные, просто возвращают void, который является first-class типом, в отличие от императивных языков. Я не специалист в этих вопросах, но для системы типов и механизма вывода типов есть теоремы, доказательства и тому подобная ерунда, которая мне совершенно не интересна, rtfm.

Конечно еще есть переменные(т.е. изменяемые значения). Они введены специально для людей с императивным мышлением, сами разработчики практически не применяют их(в коде библиотек и компиляторов) и реализованны специально с неудобным и более многословным синтаксисом. Это не мое мнение, это мнение разработчиков. Я же считаю, что они необходимы в промышленном языке, тем более для .NET. Программирование без побочных эффектов, ссылочная прозрачность и state-less объекты замечательные идеи, но сейчас и в реальной жизни они по большому счету не работают, по крайней мере не для широкого круга задач. Вот лет через десять-пятнадцать возможно они станут действительно актуальны.

Что касается макросов, то они совершенно не являются императивными. Объектный код являтся иммутабельным(т.е. нормальным функциональным типом), работа с ним происходит через term-rewriting. Единственное в чем макросы императивны это в возможности определять классы и методы, здесь действительно имеет место побочные эффекты.

А>Какой декларативный формализм лежит в основе Nemerle?

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

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

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

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

Автор: Oyster
Дата: 14.04.06

, 2) декларативного подхода на Nemerle. И в первом, и во втором случае реализуются DSL для полностью декларативного описания определенного круга задач.

Здравствуйте, Vermicious Knid, Вы писали:

VK>Здравствуйте, Аноним, Вы писали:

А>>Окамл — это типизированное по Карри-Говарду лямбда-исчисление с аппликативной редукцией

VK>Да все то же типизированное лямбда-исчисление.

Что значит все то же?
По карри-говарду? Очевидно нет. System F? только не это. Что же?
Я не понимаю, неужели так сложно дать формализм, который у Haskell и O'Caml занимает 1 абзац вместо пространных рассуждений и растеканий мыслью по древу?
Набор базовых аксиом + правила редукции и описание системы типов.
еще ближе. какая семантика у следующего кода:

class Test
{
  mutable myI : int; 
  public doit (i: int) : int
  {
    myI = i * i;
    myI;
   }
}

Что такое class? что такое mutable? что такое "public"? что из себя представляет в результате "doit"? что такое ";"? что такое "="?
Кроме того, что такое "def"? что такое "fun"?
И как это все соотносится с типизированным по Карри-Говарду лямбда-исчислением.

Здравствуйте, Vermicious Knid, Вы писали:


VK>По настоящему декларативный подход(в той интерпретации, которую я изложил выше) поддерживается только "предикативным исчислением", т.е. логическими языками. Лямбда исчисление и прочие формализмы, имеющие отношение к ФЯ это суррогат.

Да и еще, что значит суррогат? я не понимаю этого.
По вашему, любая логика высшего порядка — суррогат или только лямбда?
И с какого порядка предикаты перестают быть "по-настоящему" декларативными? предикатные переменнные — это уже суррогат или еще нет?
Полиморфные типы второго порядка — это суррогат или нет?
Чем унификация в calculus of constructions более суррогатна, чем в предикатном исчислении первого порядка?

Пожалуйста, просветите.

Здравствуйте, Аноним, Вы писали:

А>По карри-говарду? Очевидно нет. System F? только не это. Что же?
Я не поленился посмотреть определения по ключевым словам Curry-Howard и System F. Изоморфизм Карри-Ховарда это всего навсего принцип связывающий теорию типов и лямбда исчисление. Любой вид типизированного лямбда исчисления подпадает под этот изоморфизм. Ограниченный вариант типизированного лямбда-исчисления System F, система типов Хиндли-Милнера применяется в Haskell и ML, и целой куче других похожих ФЯ, так как вывод типов для System F в общем случае невозможен, а для системы Х-М есть простой алгоритм. Очевидно, что в Nemerle используется совершенно другая система типов, т.е. не Х-М и не System F, так как алгоритм вывода типов иной и довольно сложный(в силу специфический возможностей и ограничений, сейчас подробностей не помню, давно читал).

А>Я не понимаю, неужели так сложно дать формализм, который у Haskell и O'Caml занимает 1 абзац вместо пространных рассуждений и растеканий мыслью по древу?
Мне это абсолютно не интересно, формализмами я принципиально не занимаюсь. Найди на nemerle.org msc thesis разработчика Nemerle. Если он не удовлетворит твое любопытство, то спроси у него лично.

А>Набор базовых аксиом + правила редукции и описание системы типов.
А>еще ближе. какая семантика у следующего кода:
Отвечу вопросом. Приведи набор базовых аксиом + правила редукции и описание системы типов Ocaml, да так чтобы в 1 абзац уместилось. Кстати какая семантика у следующего кода?

class test = 
  object (self)
    val mutable myI = (0 : int)
  method doit i =
    myI <- i * i;
    myI
end;;

Специально для этого кода установил Ocaml(из старых дистрибутивов, в свое время я серьезно интересовался классическими ФЯ и даже чуть-чуть пописал на обычном ML, не объектном), прочитал tutorial, убедился в ряде вещей которые уже знал об этом языке. В этом отношении Ocaml ничуть не лучше Nemerle.

А>Что такое class? что такое mutable? что такое "public"? что из себя представляет в результате "doit"? что такое ";"? что такое "="?
Ко рту поднеси, да в рот положи. А может за тебя еще и разжевать, да еще и переварить?

Здравствуйте, Аноним, Вы писали:

А>Здравствуйте, Vermicious Knid, Вы писали:

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

Приведу всего один классический пример:

/* объединение пустого списка и списка L и есть список L */
append([], L, L).
/* 
   объединение списка с головой H и хвостом T, и списка L
   это новый список с головой H и хвостом, являющимся объединением T и списка L
*/
append([H|T], L, [H|R]) :-
    append(T, L, R).

А теперь аналогичный пример на Haskell(там на самом деле еще объявления полиморфных типов должны быть, но мне их писать лень)

append [] l    = l
append (h:t) l = h : (append t l)

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

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

Пример(из консоли компилятора):

?- append(X, Y, [1,2,3]).

X = []
Y = [1, 2, 3] ;

X = [1]
Y = [2, 3] ;

X = [1, 2]
Y = [3] ;

X = [1, 2, 3]
Y = [] ;

?- append(X, [1], Z).

X = []
Y = [1]
Z = [1]


?- append([1], Y, Z).

Z = [1 | Y]

?- append([1], [2], [2,3]).

No

?- append([1], [2], [1,2]).

Yes

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

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

А>По вашему, любая логика высшего порядка — суррогат или только лямбда?
Речь идет в первую очередь не о теории, а о практике. На практике в языках на базе лямбды, декларативное программирование это суррогат.

А>И с какого порядка предикаты перестают быть "по-настоящему" декларативными? предикатные переменнные — это уже суррогат или еще нет?
Предикаты не перестали быть декларативными, я этого не говорил.

А>Полиморфные типы второго порядка — это суррогат или нет?
Вроде бы поддерживаются в Nemerle.

А>Чем унификация в calculus of constructions более суррогатна,
Честно говоря мне лень рыться в терминах и отвечать на все эти вопросы. Я не настолько упрям и не претендую на роль гуру в computer science.

А>чем в предикатном исчислении первого порядка?
Есть кстати логические языки с предикатным исчислением более высокого порядка, чем в Prolog.

А>Пожалуйста, просветите.
"Просветить" это ваша специальность, вы ведь занимаетесь computer science, а не я. Так что идите просвещать, только не здесь. Для этого есть высшие учебные заведения и другие места.

Здравствуйте, Аноним, Вы писали:

А>Набор базовых аксиом + правила редукции и описание системы типов.
А>еще ближе. какая семантика у следующего кода:
А>

А>class Test
А>{
А>  mutable myI : int; 
А>  public doit (i: int) : int
А>  {
А>    myI = i * i;
А>    myI;
А>   }
А>}
А>

А>Что такое class? что такое mutable? что такое "public"? что из себя представляет в результате "doit"? что такое ";"? что такое "="?
А>Кроме того, что такое "def"? что такое "fun"?
А>И как это все соотносится с типизированным по Карри-Говарду лямбда-исчислением.

Скажу за себя. Я индустриальный инженер, и мне совершенно плевать, как "это" соотносится с типизированным по Карри-Говарду лямбда-исчислением. Мне главное, чтобы в разработке дешевле было, и плевать на твои формализмы. Мне этот код понятен, писать на Немерле я смогу легко. Так же, как и на Haskell, ML, Erlang, Clean, C++, Java, FORTH, FORTRAN, you name it. Вопросов к семантике у меня нет.

Даже для использования и понимания хаскельных монад не надо знать теорию категорий, а ты говорить о коде в духе Hello World, и жалуешься, что тебе его семантика не понятна. Смешно. Ты, наверно, решаешь в уме дифференциальные уравнения, чтобы управлять своим автомобилем? По другому не понятно, как баранку крутить, да?

Здравствуйте, <Аноним>, Вы писали:

Чего-то мне это всё напоминает. Возвращение редуктора?

Здравствуйте, <Аноним>, Вы писали:

А>По карри-говарду?

По карингу тебе говорили уже. Его нет, так как есть С-шный синтаксис вызова функций, перегрузка функций/метдов и неявные приведения типов.

В Лиспе и Схеме карринга тоже нет, но это не мешает им считаться ФЯ.

А>Я не понимаю, неужели так сложно дать формализм, который у Haskell и O'Caml занимает 1 абзац вместо пространных рассуждений и растеканий мыслью по древу?

А>Набор базовых аксиом + правила редукции и описание системы типов.

По поводу вывода типов:
http://nemerle.org/~malekith/msc.pdf

А>Что такое class? что такое mutable? что такое "public"? что из себя представляет в результате "doit"? что такое ";"? что такое "="?

Это синтаксис языка. Точнее отдельные его части. Собственно аналогичные вещи есть и в ОКамле. Например, весто ";" в нем используется ",". Суть та же — отделение выражений. Есть в нем и классы.

А>Кроме того, что такое "def"? что такое "fun"?

А пойти почитать на сайт? "fun" — это аналог ML-ного fn, то есть синтаксис лямбды.
def — это нечто вроде "let ... in@.

А>И как это все соотносится с типизированным по Карри-Говарду лямбда-исчислением.

Напрямую. Иди прочти руковдство по языку прежде чем производить сравнение с ним.