Хотя что-то не могу найти подтверждения, так что скорее всего соврал относительно Haskell.
Тем не менее всякие структуры данных и алгоритмы работы с ними 1 в 1 пишутся на той же Agda.
А нам не нужно для произвольных, нам для конкретных.
Завершимость тоже не определишь в общем случае, что не помешало определить её для, ЕМНИП, 80% стандартной библиотеки Haskell.
Например для Haskell есть Zeno, генерирующий доказательство на Isabelle. По ссылке уже написан тестовый код на Haskell и утверждения, которые надо доказать. По умолчанию там выбран isorts_sorts:
Которые слизаны с ФП как раз. Но я отвечал на «Объясните мне, как элегантно решить данную задачу без ООП». Однако я не согласен с утверждением «И в ООП нет ничего, что позволяет решать ту или иную задачу элегантнее», тем не менее всё вполне решается и без наличия в самом языке классов или методов. Особенно если учесть, что ООП — это подход. Тот же Erlang вообще вполне себе ООП (процессы обмениваются сообщения), и на том же Haskell можно сделать ООП через зелёные потоки. Так что сам подход иногда очень хорошо ложится на задачу, но это не значит, что ООП нужен везде, и уж тем более не значит, что без поддержки в языке классов в нём будет что-либо неудобно.
К сожалению, у меня нет времени тут расписывать всё это.
Это «интерфейс», реализуя который мы получаем функцию сравнения двух объектов.
Отличие от x.isEqual(y) в том, что isEqual реализован для object и принимает object, поэтому равенство типов приходится проверять внутри самому. Тут же == гарантированно принимает значения одного типа. А вот какого именно — уже неважно.
Я же написал выше про классы типов, они шире интерфейсов.
Что такое реализовать интерфейс? Предоставить набор функций над конкретным типом данных. В ФП это делается тривиально.
Нет, я предлагаю ознакомиться с тем, как реализована инкапсуляция и полиморзфим в неООП. Тогда вы сами поймете, как эти задачи решаются там.
То же, что вы сейчас написали выше, не дико не удобно, а ровно то ООП и есть, только с другим синтаксисом.
Что значит «выводилка загрустит»? Работать перестанет? Станет тормозить?
По опыту скажу, что в реальной программе куда быстрее загрустят люди, которым информация о типе многое говорит, и хорошо было бы этот тип видеть глазами. А вот выводилка чувствует себя хорошо.
Пока вы формулируете задачу в терминах ООП через «я создаю классы» и «у них есть методы», я не смогу вам ответить, так как в ФП нет методов, а есть функции, поэтому сама задача «три класса с одинаковыми методами» там звучит крайне странно.
Вот, например, хотим мы уметь сравнивать числа, строки, whatever you want, в Haskell для этого существует класс типов Eq, это похоже на интерфейсы, но несколько мощнее
class Eq a where
(==) :: a -> a -> Bool
-- обратите внимание на то, что с обоих сторон от == значения одного типа
-- т.е. написать 1 == "asd" нельзя, а вот 1 == 2 и "sdd123" == "34sdf" - можно
Причём реализовано это через обычную структуру, вот такую:
data Eq a = Eq { (==) :: a -> a -> Bool }
Разница только в том, что во втором случае мне придётся её передавать в функции явно, а класс типов передаётся неявно.
Вот статическая типизация:
foo x = x + 1
Избыточный синтаксис нужен не при статической типизации, а при обязательной декларации типов, но это не обязательно присутствует в статически-типизируемом языке.
You can only compile modules without unsolved metavariables
or termination checking problems.
Тем не менее всякие структуры данных и алгоритмы работы с ними 1 в 1 пишутся на той же Agda.
Завершимость тоже не определишь в общем случае, что не помешало определить её для, ЕМНИП, 80% стандартной библиотеки Haskell.
На Agda можно заниматься тем же самым вручную. Там first-class доказательства, основанные на изоморфизме Карри-Говарда.
Я ради интереса вбивал туда монадические законы для Maybe, List и т.п.
Это «интерфейс», реализуя который мы получаем функцию сравнения двух объектов.
Отличие от x.isEqual(y) в том, что isEqual реализован для object и принимает object, поэтому равенство типов приходится проверять внутри самому. Тут же == гарантированно принимает значения одного типа. А вот какого именно — уже неважно.
Через isEqual что ли с принятием 2-х object?
Что такое реализовать интерфейс? Предоставить набор функций над конкретным типом данных. В ФП это делается тривиально.
То же, что вы сейчас написали выше, не дико не удобно, а ровно то ООП и есть, только с другим синтаксисом.
Правда на деле это крайне редко нужно, потому что на ФП разрабатывают иначе.
По опыту скажу, что в реальной программе куда быстрее загрустят люди, которым информация о типе многое говорит, и хорошо было бы этот тип видеть глазами. А вот выводилка чувствует себя хорошо.
Вот, например, хотим мы уметь сравнивать числа, строки, whatever you want, в Haskell для этого существует класс типов Eq, это похоже на интерфейсы, но несколько мощнее
Причём реализовано это через обычную структуру, вот такую:
Разница только в том, что во втором случае мне придётся её передавать в функции явно, а класс типов передаётся неявно.
foo x = x + 1
Избыточный синтаксис нужен не при статической типизации, а при обязательной декларации типов, но это не обязательно присутствует в статически-типизируемом языке.