Снова макросы Racket

Для них если типы совпадают - значит и семантика совпадет

Да ладно, никто так не считает, это как в твиттере Кармака, хотя на практике всё падает только так независимо от типов — вопрос в прилежности программистов (вот сейчас как раз сталкиваюсь — старые поделки с hackage для анализа prof, например, падают, и threadscope не всегда работает из-за каких-то жоп из binary). Если семантика и совпадает, то только в том, что функции из пространства Int -> Int, например, принимают числа фиксированной точности (или _|_) и возвращают числа фиксированной точности (или _|_), больше ничего тут нельзя сказать. Поэтому существуют такие вещи как QuickCheck — для тестирования семантики, типы класса Arbitrary рандомно генерируют свои значения, поставляют в функции, результаты сверяются с заявленными аксиомами (такие зависимые типы для бедных). В агде аналогично — ListSort = forall {T} -> List T -> SortedList T значит только то что значит — если sort : ListSort пишется, то _существует_ процесс сортировки привязанный к этим типам, доказательств-алгоритмов (sort) может быть множество, они отличаются как минимум операционной семантикой (той же сложностью), хотя денотационная уже более-менее зафиксирована (тоже не без проблем).

То есть абстрактные интерфейсы в хаскеле и в некоторых других распостранённых языках — только приближение к нужным интерфейсам (класс типов Monoid ничего не знает про ассоциативность и идентичность единицы, например). В CL defgeneric — ещё более грубое и свободно-интерпретируемое приближение.

Насчёт общих интерфейсов и переписывания — это как бы не только в хаскеле так, есть стандартная библиотека скалы (+ algebird, bijection, scalaz и т.п.), есть стандартная библиотека плюсов (в смысле экс-STL, которая изначально вообще для схемы писалась). Есть общие интерфейсы, есть обобщённый код который использует _только_ такие интерфейсы, если конкретный тип умеет какой-то обобщённый интерфейс, значит он сразу автоматически умеет и весь производный код — его можно утилизировать для этого типа, а не писать снова.

Имелись в виду карринг и частичное применение (и потом такие функции передаются в compose) — ((map add1) xs) ~ (map add1 xs), (compose (map add1) (map sub1)) == identity. (>=>) это обобщение compose.

Да ладно, никто так не считает

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

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

Вот об этом я и говорю. Тип подходит, законы функтора выполняются - значит функтор. А до того, что семантики функтора нету и близко - хаскелистам и дела нет никакого.

Насчёт общих интерфейсов и переписывания — это как бы не только в хаскеле так

Только в хаскеле.

сть стандартная библиотека скалы (+ algebird, bijection, scalaz и т.п.), есть стандартная библиотека плюсов

В библиотеках плюсов и скалы ничего абстрактного/обобщенного нет. scalaz - это да, но scalaz не более чем бесполезная игрушка для людей, которые захотели чтобы было «как в хаскеле».

Есть общие интерфейсы, есть обобщённый код который использует _только_ такие интерфейсы, если конкретный тип умеет какой-то обобщённый интерфейс, значит он сразу автоматически умеет и весь производный код — его можно утилизировать для этого типа, а не писать снова.

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

Все определяется по семантике, а не по типу и абстрактным законам, которые должны выполняться. Вот например если у нас есть какой-нибудь iterable[A], то он и будет определяться для вещей семантически соответствующих типу данных, по которому можно итерироваться. Несмотря на то, что формально его можно определить практически для чего угодно. И в результате не получается диких вещей типа того, что список является монадой.

Список, например, семантически не монада

module List where

open import Level
open import Relation.Binary.PropositionalEquality hiding ( [_] )

import Categories.Functor as F
open import Categories.Monad
open import Categories.Agda

Type = Sets zero

TypeFunctor = F.Endofunctor Type

open import Data.List
open import Data.List.Properties

List-is-Functor : TypeFunctor
List-is-Functor = record
  { F₀ = List
  ; F₁ = map
  ; identity = λ {_ xs} → map-id xs
  ; homomorphism = λ {_ _ _ _ _ xs} → map-compose xs
  ; F-resp-≡ = λ p {xs} → map-cong (λ z → p {z}) xs
  }

open import Category.Monad
open RawMonad (monad {zero})

List-is-Monad : Monad Type
List-is-Monad = record
  { F = List-is-Functor
  ; η = record
    { η = λ _ → [_]
    ; commute = λ _ → refl
    }
  ; μ = record
    { η = λ _ → join
    ; commute = λ f {xss} → commute₂ {f = f} xss
    }
  ; assoc = λ {_ xsss} → assoc xsss
  ; identityˡ = λ {_ xs} → identityˡ xs
  ; identityʳ = λ {_ xs} → identityʳ xs
  } where

    commute₂ : {X Y : Set} {f : X → Y} (xss : List (List X)) → join (map (map f) xss) ≡ map f (join xss)
    commute₂ [] = refl
    commute₂ ([] ∷ xss) = commute₂ xss
    commute₂ {f = f} ((x ∷ xs) ∷ xss) = cong (_∷_ (f x)) (commute₂ (xs ∷ xss))

    assoc : {X : Set} (xsss : List (List (List X))) → join (map join xsss) ≡ join (join xsss)
    assoc [] = refl
    assoc ([] ∷ xs) = assoc xs
    assoc (([] ∷ xs) ∷ xss) = assoc (xs ∷ xss)
    assoc (((x ∷ xs) ∷ xss) ∷ xsss) = cong (_∷_ x) (assoc ((xs ∷ xss) ∷ xsss))

    identityˡ : {X : Set} (xs : List X) → join (map [_] xs) ≡ xs
    identityˡ [] = refl
    identityˡ (x ∷ xs) = cong (_∷_ x) (identityˡ xs)

    identityʳ : {X : Set} (xs : List X) → join [ xs ] ≡ xs
    identityʳ [] = refl
    identityʳ (x ∷ xs) = cong (_∷_ x) (identityʳ xs)

open import Categories.Functor.Algebra
open import Categories.Functor.Algebras

open import Data.Unit

List-F-Algebra-example : F-Algebra List-is-Functor
List-F-Algebra-example = record
  { A = ⊤
  ; α = λ _ → tt
  }

open import Categories.Category

List-F-Algebras-Category : Category _ _ _
List-F-Algebras-Category = F-Algebras List-is-Functor

open import Categories.Object.Initial

List-initial-F-Algebra : Initial List-F-Algebras-Category
List-initial-F-Algebra = {!!}

open Lambek List-initial-F-Algebra

open import Categories.Monad.Kleisli

List-Kleisli-Category : Category _ _ _
List-Kleisli-Category = Kleisli List-is-Monad

open import Categories.Grothendieck

List-Grothendieck-Category : Category _ _ _
List-Grothendieck-Category = Grothendieck List-is-Functor

-- Eilenberg-Moore, List-is-Monad ≊ Right-Adjoint-F-Algebras-Type-Representation ∘ Left-Adjoint-Free-F-Algebras-Generator, etc.

Опровергай.

Или комопозиция - это не функтор

open import Function

postulate
  ext : Extensionality zero zero

→-is-Functor : ∀ {R} → TypeFunctor
→-is-Functor {R} = record
  { F₀ = (λ A B → A → B) R
  ; F₁ = _∘′_
  ; identity = refl
  ; homomorphism = refl
  ; F-resp-≡ = λ p {h} → ext (λ x → p {h x})
  }

В библиотеках плюсов и скалы ничего абстрактного/обобщенного нет

Ну может быть, итераторы и функциональные объекты в С++ более конкретны и не настолько общие, но всё равно — любой класс можно сделать функтором или итератором, так что все обобщённые алгоритмы заведутся как нам хочется. Также как и в скале с Function*, Iterator / Iterable.

Опровергай.

Опровергать что? Ты только что подтвердил мое мнение - для хаскелиста достаточно выполнения формальных условий (соответствия типов, исполнения абстрактных законов) и все. И вот будет он талдычить что список - это монада, раз _формально_ тип данных «список» нужным законам удовлетворяет. А то, что с точки зрения семантики - это полная бессмыслица - ему невдомек, и никак он понять не сможет, почему же maybe - монада, а список - нет.

Для хаскелиста два объекта, обладающих одинаковыми свойствами - это один и тот же объект. Хаскелист не понимает, что эти два объекта могут использоваться по-разному и только этим (своим назначением, семантикой, то есть) будут отличаться. И тем более ему не понять, что как раз это отличие - первично, а никакие не свойства. Так что сколько хаскелисту не объясняй, а он никогда не поймет, что называть одним словом map для АТД и композицию нельзя, т.к. это вещи, семантически не имеющие ничего общего.

Ну может быть, итераторы и функциональные объекты в С++ более конкретны и не настолько общие

Именно! Потому что там все определяет семантика.

но всё равно — любой класс можно сделать функтором или итератором

Именно! Но не делают. Потому как это будет ошибка. Но монад, кстати, в плюсах уже не сделаешь.

Для хаскелиста два объекта, обладающих одинаковыми свойствами - это один и тот же объект.

Пример - документ с гербовой печатью и клочок туалетной бумаги для хаскелиста одно и то же: «бумага». И обращаться он с ними будет одинаково. Объект же один. То, что для любого здорового человека очевидно не то что различие а вообще несравнимость этих объектов - хаскелист аргументом не считает, т.к. у него есть замечательный контраргумент - подтирать жопу можно и важными документами. Следовательно, любой документ - есть частный случай туалетной бумаги.

ему невдомек, и никак он понять не сможет, почему же maybe - монада, а список - нет.

Ну так почему? О каких «монадах» и «семантиках» тогда идёт речь?

Конкретно список вроде '(1 2 3) или nil так же как и функция compose это, верно, не монады — монады это [построения над построениями над] конструкторы типов List : Type -> Type и forall T. (-> T) : Type -> Type, которые будучи функторами уже доставляют map и compose (может, просто нехаскелисту никак не понять таковой концепции любой тип -> новый тип по некоторой схеме его formation, introduction, elimination & computation).

Но монад, кстати, в плюсах уже не сделаешь

Почему нет?

Ловко подменил понятия, A <: C, B <: C => A <: B, молодец.

Конкретно список вроде '(1 2 3) или nil так же как и функция compose это, верно, не монады — монады это [построения над построениями над] конструкторы типов List : Type -> Type и forall T. (-> T) : Type -> Type, которые будучи функторами уже доставляют map и compose (может, просто нехаскелисту никак не понять таковой концепции любой тип -> новый тип по некоторой схеме его formation, introduction, elimination & computation).

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

Почему нет?

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

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

Неправильно! Монада в программировании - это абстракция связывания вычислений.

Это где такое определение? Интуитивное определение — штука с состоянием, позволяюющая указывать вычисления изменяющие это состояние.

И в этом смысле

thirdConfigs bd = do
  bd1 <- nextConfigs bd
  bd2 <- nextConfigs bd1
  bd3 <- nextConfigs bd2
  return bd3

Вполне себе описание последовательности состояний списка. Или list comprehension (это к вопросу «зачем полседовательность состояний списку?»).

Кстати, аналогично, Iterable в некоторых языках определён для всех классов. Действие по-умолчанию — перебор полей объекта. Тоже будешь говорить, что это неверно и конструкция foreach (field in rabbit) не должна существовать?

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

Если мы рассматриваем объект только с точки зрения подтирания, то да.

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

Монада в программировании

Фтопку же, какие-то свои уездные «монады в программировании».

Ты так и не объяснил интуицию — чем список хуже Maybe? «Список id юзеров -> список структур юзеров -> список имён юзеров» или «может id юзера -> может структура юзера -> может имя юзера» — какая разница? Если не нравится делать map f g для функций — можно делать им f <$> g, или f `ohShitThisIsSoGeneric` g.

В плюсах нету ограниченной квалификации.

Ок, это называется «концепты», которые не взлетели (http://www.pik-potsdam.de/members/lincke/papers/Lincke_et_al_SCP.pdf). Но вообще изобразить можно — на гитхабе где-то была библиотека полная эзотерических извращений на C++11.

Я ничгео не подменял. Обычная логика хаскелиста

Скажи им что у них сломанная логика :)

на гитхабе где-то была библиотека

http://github.com/beark/ftl