Как в Lisp передать функцию ссылку на объект?

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

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

Тот пост был о субъективизме трех вполне конкретных понятий.

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

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

Уж совсем унылый спор пошёл...

Уже выше писали: в «статике» (особливо - в хаскеле) ты значительную часть логики «программируешь типами», а если ты так не делаешь, то ты «забиваешь гвоздь микроскопом». И ситуация со списком разных примитивных типов - это или «обычный быдлокод», или, если это действительно надо именно в таком виде, оформляется в отдельный «модуль», обкладываемый снаружи железобетонным саркофагом типов. Подобный публичный API в хаскеле - «ну если за такое не убивать, то...» :)

Но «программировать типами» - не всем нравится. Мне вот не нравится совершенно (не смотря на то, что я осознаю «профиты») - и потому мне больше по душе CL с его «типо-свободой»: можешь обписаться на CLOS-е, получив тот-же type-check во время компиляции (вот только вывода типов, можно сказать, нет), а можешь полностью забить на типы, не забывая просто проверять их корректность в «точках соприкосновения».

Но это совершенно субъективные вопросы «удобства» для каждого отдельного индивидуума.

задачу, где ты это делаешь и откуда у тебя список из разных примитивных типов?

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

Как «обработанный» список ты будешь использовать дальше?

Как угодно.

Уже выше писали: в «статике» (особливо - в хаскеле) ты значительную часть логики «программируешь типами»

Это неправда. На данный момент нету используемых на практике ЯП, в которых типами можно кодировать хоть какую-то логику.

И ситуация со списком разных примитивных типов - это или «обычный быдлокод»

Да нет, это вполне обычная задача, которая требует размеченных объединений. Или их в язык добавили специально для быдлокодеров?

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

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

Но «программировать типами» - не всем нравится.

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

Дело в том, что нету самого такого понятия - «программирование типами».

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

На данный момент нету используемых на практике ЯП, в которых типами можно кодировать хоть какую-то логику.

«хоть какую-то» - если в смысле «любую первую встречную» - да, нет таких. Но специфическую часть алгоритма - можно. Как минимум - ту-же проверку типов.

это вполне обычная задача, которая требует размеченных объединений

это как требование на CL написать вектора «с прямым доступом к памяти» - это уже РЕШЕНИЕ х.з. какой задачи, т.е. явный костыль в проектировании решения задачи на хаскеле.

При чем никакого профита от этого обкладывания мы не получаем, только тратим свое время. И в чем смысл тогда?

Ты не получаешь профита и не видишь смысла. Кто виноват?

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

Можешь привести контрпример в котором будет неоднозначность?

Я приводил

enum ab { a = p, b };
enum cd { c = q, d };

data AB = A | B
data CD = C | D

объединяй однозначно.

Что непонятного?

Непонятно почему ты пытаешься связать с передачей nothing внештатную ситуацию — передаётся optional value, если оно nil / Nothing, то делается что-то одно (ничего не делается, например, сообщения не будут слаться супервизору, логи будут писаться в default.log, сервер забиндится на 127.0.0.1, и т.п.), если передаётся нормальное value != nil / Just value — что-то другое (что-то будет делаться — слаться сообщения на переданную под Just ноду, будет писаться в лог переданный под Just, bind будет делаться по данному адресу под Just и т.п.).

Ну и хаскель - «апофигей апофеоза», где большая часть кода - описание типов, но таки несущая функциональную нагрузку.

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

Но специфическую часть алгоритма - можно.

Нельзя, в том и дело.

это как требование на CL написать вектора «с прямым доступом к памяти» - это уже РЕШЕНИЕ х.з. какой задачи, т.е. явный костыль в проектировании решения задачи на хаскеле.

Да при чем тут костыль? Я не понимаю, почему ты называешь костылем стандартное для хаскеля решение (использование размеченных объединений)?

Ты не получаешь профита

Никто не получает.

с твоими эмоциями на грани истерики.

Лол.

AB | CD = A | B | C | D, какие проблемы? У всех енумы работают и прекрасно однозначно объединяются, но вот пришел quasimoto и открыл глаза, лол.

Ты сам посмотри то на свое определение. Неразмеченное объединение - это просто sup, с чего он у тебя в решетке сабтайпинга неоднозначно определен будет?

Непонятно почему ты пытаешься связать с передачей nothing внештатную ситуацию

Потому что на практике его в 99% случаев используют для прикрытия дырки в нештатной ситуации. Всегда, когда ты работаешь с maybe в монаде - ты прикрываешь дырку в исключительной ситуации с потерей информации о том, что, собственно, приключилось. Когда ты матчишь пришедшее сообщение, которое может быть nothing, то это аналог catch-блока (на Nothing) или идущего вслед за всем try-блоком кода. Проблема в том, что код _внутри_ try-блока не всегда состоит из одной ф-и. Обычно nothing (или исключение) происходит где-то глубоко внутри, а ловим (матчим к nothing) мы его через нцать вызовов.

какие проблемы?

Начни с примера на C++ лучше:

enum ab { a = p, b };
enum cd { c = q, d };
union abcd { ab x; cd y; abcd(ab x_) : x(x_) {} abcd(cd y_) : y(y_) {} };

Что если p == q? Тогда a == c, b == d и в abcd только два _разных_ (not equal) элемента — a == c == p == q и b == d == p + 1 == q + 1. Если теперь abs(p - q) = 1, то там три различных элемента. Иначе — четыре.

Стандарт говорит что enums promoted to integers, но оставляет за реализацией выбор конкретного типа, допустим, что это int, тогда всё это работает за счёт того, что ab и cd — подтипы int, то есть есть инъекции из них в int, на int есть equality, так что _между_ ab и cd оно есть — как подмножества int они прекрасно и однозначно объединяются, но только _после_ того как конкретные инъекции, то есть значения p и q, выбраны и, таким образом, задано equality _между_ ab и cd.

У всех енумы работают и прекрасно однозначно объединяются

Как видишь, в C и C++ они зависят от того _как именно_ enums promoted to integers, то есть от того как задано межтиповое equality.

Если теперь взять

data AB = A | B
data CD = C | D

то кто сказал, что B != C, например? Equality между AB и CD не задано, могут быть разные типы ABCD для которых AB <: ABCD и CD <: ABCD, то есть разные инъекции из этих типов в объединение:

A B C D
* * * *
| | | |
* * * *
// твой вариант

A B   C D
* *   * *
|  \ /  |
*   *   *
    B == C

A B C D
* * * *
 \ X /
  * *
A == C
    B == D

...

если взять

class a :~ b where
  isEqual :: a -> b -> Bool

и выбрать нужные

instance AB :~ CD where ...
instance CD :~ AB where ...

то можно зафиксировать equality между AB и CD, тогда, и только _после_ этого, опять, можно будет выбрать конкретное объединение. Это можно сделать более чем одним способом:

{-# LANGUAGE TypeOperators, MultiParamTypeClasses #-}

data AB = A | B deriving Eq
data CD = C | D deriving Eq

class a :~ b where
  isEqual :: a -> b -> Bool

instance AB :~ AB where
  isEqual = (==)

instance CD :~ CD where
  isEqual = (==)

-- * Одно объединение.

instance AB :~ CD where
  _ `isEqual` _ = False

instance CD :~ AB where
  _ `isEqual` _ = False

{-
*Main> A `isEqual` A
True
*Main> A `isEqual` B
False
*Main> A `isEqual` C
False
*Main> A `isEqual` D
False
-}

-- * Другое.

instance AB :~ CD where
  B `isEqual` C = True
  _ `isEqual` _ = False

instance CD :~ AB where
  C `isEqual` B = True
  _ `isEqual` _ = False

{-
*Main> B `isEqual` C
True
*Main> C `isEqual` D
False
*Main> C `isEqual` B
True
*Main> A `isEqual` D
False
-}

Абстрактный ADT индуцируется функтором. Например, 1 -> 1 + 1 задаёт класс эквивалентности которому принадлежат эти AB и CD — пока не задано equality (и не путаем с equivalence) _между_ ними, то есть они не вложены мониками (которых много разных в любом сколько-нибудь сложном случае, вот даже для AB и СВ) в какой-то общий супертип с уже обычным внутритиповым equality термов — никаких однозначных объединений.

Ты сам посмотри то на свое определение

Да, в нём результат зависит от того какие именно A ⊆ C и B ⊆ C находятся в данном контексте (там implicit arguments) — а их можно написать разных, очевидно.

с чего он у тебя в решетке сабтайпинга неоднозначно определен будет?

У тебя слишком сильный базис — решётка сабтайпинга со всюду известным equality (Any * Any -> Bool), как в этой самой теории множеств. В этом смысле Scala интересна — решётка (ну или предпорядок лучше) есть, equals есть у Any, то есть у всего, так что:

abstract class AB
case class A() extends AB
case class B() extends AB

abstract class CD
case class C() extends CD
case class D() extends CD

и, как ты и говоришь:

scala> A.equals(C)
res1: Boolean = false

scala> A.equals(D)
res2: Boolean = false

scala> B.equals(C)
res3: Boolean = false

scala> B.equals(D)
res4: Boolean = false

но:

scala> new B {
  override def equals(obj: Any) =
    this.isInstanceOf[B] && obj.isInstanceOf[C] ||
    this.isInstanceOf[C] && obj.isInstanceOf[B] ||
    super.equals(obj)
}.equals(new C)
res7: Boolean = true

в самих определениях case class тоже можно переписать, разумеется. То есть _даже_ если у тебя решётка типов и полное equality повсюду на Any — есть неоднозначность, точнее варьируемость — можно реализовать своё понятие equality которое изменит объединение, как я говорил — может захотеться отождествлять списки с какими-то деревьями, например (интересно, что в лиспе списки и деревья суть всё cons-ы), чтобы они отождествлялись и в объединении, это можно сделать несчётным количеством способов.

Потому что на практике его в 99% случаев используют для прикрытия дырки в нештатной ситуации

http://hackage.haskell.org/packages/archive/mtl/latest/doc/html/Control-Monad...

instance MonadError () Maybe where
  throwError _ = Nothing
  Nothing `catchError` h = h ()
  j `catchError` _ =  j

я что-то не вижу. Ты описываешь MaybeT и ErrorT (EitherT), с типами Maybe и Either «на практике» всё просто (иначе — плохие сигнатуры с ссылками на haddock в студию), их «в монаде» никто не использует, это просто суммы, чтобы их толком можно было использовать «в монаде» — нужен трансформер (который уже может эмулировать исключения на Maybe/Either, да). Причём MaybeT и ErrorT это просто конкретные реализации интерфейса MonadError, так же как и «обычные» исключения IOException в IO и их возможные производные.

Что если p == q? Тогда a == c, b == d и в abcd только два _разных_ (not equal) элемента — a == c == p == q и b == d == p + 1 == q + 1. Если теперь abs(p - q) = 1, то там три различных элемента. Иначе — четыре.

Ну и что, что p = q? Ты говоришь об элементах, а элементов у нас вообще нет.

Как видишь, в C и C++ они зависят от того _как именно_ enums promoted to integers, то есть от того как задано межтиповое equality.

Ничуть не зависят.

то кто сказал, что B != C, например?

Ну пусть B = С.

Equality между AB и CD не задано

Как же не задано? Задано.

могут быть разные типы ABCD для которых AB <: ABCD и CD <: ABCD, то есть разные инъекции из этих типов в объединение

Типы то могут быть и разные, но вот sup один.

// твой вариант

Эти варианты эквивалентны.

если взять

А не надо брать. Нам equality жестко задано в самом языке.

можно будет выбрать конкретное объединение. Это можно сделать более чем одним способом:

Нет, только одним.

Например, 1 -> 1 + 1 задаёт класс эквивалентности которому принадлежат эти AB и CD — пока не задано equality (и не путаем с equivalence) _между_ ними

Так оно строго задано в языке.

Да, в нём результат зависит от того какие именно A ⊆ C и B ⊆ C находятся в данном контексте (там implicit arguments) — а их можно написать разных, очевидно.

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

У тебя слишком сильный базис — решётка сабтайпинга со всюду известным equality

Да откуда ты equality выдрал? Его вообще в решетке нету и быть не должно. Решетка требует однозначного sup сама по себе, equality она не требует. Если у нас есть решетка - то мы всегда можем брать однозначный sup. По определению. Если не можем - это не решетка. Но если у тебя сабтайпинг не дает решетку - то это проблемы твоего очень хуевого сабтайпинга. И, еще раз, никакого equality нет и не надо.

В этом смысле Scala интересна — решётка (ну или предпорядок лучше) есть, equals есть у Any, то есть у всего, так что:

Если убрать из скалы equals и Any ничего не изменится - типы так же будут образовывать решетку и мы так же сможем брать однозначный sup.

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

То есть Maybe - не монада? Ну-ну.

То есть _даже_ если у тебя решётка типов и полное equality повсюду на Any — есть неоднозначность

Если у тебя есть решетка типов то у тебя НЕ МОЖЕТ быть неоднозначности. По определению решетки.

Да, в любом ЧУП задано equality: A = B <=> A < B and B < A, и поменять его нельзя.

Ты говоришь об элементах, а элементов у нас вообще нет.

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

Ну пусть B = С

Пусть нет — {a, b} U {c, d} = {a, b, c, d}, пусть да — {a, b} U {c, d} = {a, b (= с), d}. И не надо рассказывать, что между 3 и 4 есть биекция (мол, они «эквивалентны»).

Прикинь, размеченное объединение типов A и B тоже зависиит от типов A и B.

Это понятно, речь о том, что помимо этого есть зависимость от стороннего equality (которое задаётся функциями в _⊆_ в том примере).

Да откуда ты equality выдрал?

А откуда ты решётку выдрал? Но если у тебя всё по решётке — тогда да, только это не интересно, так как оставляет без внимания ситуации когда нужно смотреть дальше — на элементы типов и на их равенство, в том числе на возможность разных интерпретаций — {a, b} ~ (range 1 2) <: int, например, или любая другая пара чисел из int.

То есть Maybe - не монада?

Монада, но я сказал несколько другое — что монадический интерфейс к Maybe не используется. Или используется? Какой-нибудь пример работы в котором Maybe мучают в do-нотации в разных функциях, так что это нехорошим образом напоминает эмуляцию исключений?

Если взять пример с Name/Surename для Скалы который эксплатируется в блогах, что-то такое:

abc :: Maybe a -> Maybe b -> Maybe c -> Maybe (a, b, c)

там пишут через for, то есть аналогично

abc x y z = do { x' <- x; y' <- y; z' <- z; return (x', y', z') }

хотя аппликативного интерфейса тут достаточно:

abc x y z = (,,) <$> x <*> y <*> z

или

abc = liftA3 (,,)

Другой пример — построить

data ABC = ABC String String String deriving Show

из environment используя дефолтные значения и валидирующие предикаты, тут тоже не нужен монадичесий интерфейс:

abc :: IO (Maybe ABC)
abc = ABC <$$> maybe False (all isDigit) <?$> getEnv "a" <**> getEnv "b" <||> pure2 "default b" <**> getEnv "c"

монадический интерфейс может понадобится для дополнительного разбора, например

data ABC = ABC Integer String (Integer, Char) deriving Show

хотя оно всё ещё вполне декларативно:

abc :: IO (Maybe ABC)
abc = ABC <$$> readMay =<<$ getEnv "a" <**> getEnv "b" <||> pure2 "default b" <**> readMay =<<$ getEnv "c"

потом где-то добавляется единственный фильтр после которого существует уже чистое ABC.

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

Не может. Потому что объединение не зависит от равенства и от элементов. На самом деле, если у нас есть сабтайпинг и Any, то мы всегда можем определить A | B = Any и получим, таким образом, вполне корректные (но тривиальные, и потому неинтересные) объединения.

Пусть нет — {a, b} U {c, d} = {a, b, c, d}, пусть да — {a, b} U {c, d} = {a, b (= с), d}.

Так тип это же не множество.

И не надо рассказывать, что между 3 и 4 есть биекция (мол, они «эквивалентны»).

Ну в том и дело, что они эквивалентны. Ты рассматриваешь множества, а нам то надо не о множествах говорить, а о типах этих множеств и о равенстве типов. Пусть Tx - минимальный тип, являющийся типом, содержащим множество х, тогда T{a, b, c, d} = T{a} | T{b} | T{c} | T{d}, если b = c (в смысле рефлексивности идентичности, а не в смысле того что для них выполняется абстрактное equality), то очевидно T{b} = T{c}, т.к. T{a} = T{a}. Но может быть и такое, что T{b} = T{c}, b !=c (например T{2} = Int = T{4}). И нам важно не равенство на элементах х, а равенство на Tx, которое строго задается самим ЧУП (фактом принадлежности элементов типам и более ничем) и не может варьироваться (т.к. мы не можем объявить «пусть к этому типу добавится такое-то значение» - это сломало бы систему типов).

Это понятно, речь о том, что помимо этого есть зависимость от стороннего equality

Нету. Откуда вообще ты взял equality? Нам нужна только верхняя грань, никакого equality.

А откуда ты решётку выдрал?

Ну потому что на практике это решетка.

тогда да, только это не интересно

Но так есть на практике.

без внимания ситуации когда нужно смотреть дальше — на элементы типов и на их равенство

А нам не надо смотреть на элементы типов, потому что мы вообще о них ничего на знаем. У нас есть некое абстрактное ЧУП (типы и отношение подтипирования), при чем <= задано в этом ЧУП так, что мы можем однозначно определять sup. Объединение типов не обязательно должно соответствовать объединению множеств (более того, оно в общем и не может), Просто потому, что нету биекции между множествами и типами. Нету даже вложения из типов в множества (разным типам может соответствовать одно множество) и сюрьекции множеств на типы (т.к. не любому множеству соответствует тип).

И никакого equality, повторяю, нет просто потому, что элементов нет, а значит и применять equality не к чему. На типах же equaliti обязано определяться как A = B <=> A <= B && B <= A, иначе у нас не то что не решетка, а даже не ЧУП.

Или используется? Какой-нибудь пример работы в котором Maybe мучают в do-нотации в разных функциях, так что это нехорошим образом напоминает эмуляцию исключений?

Только так и используется. Практически любой пример.

там пишут через for, то есть аналогично

Так for скалы это и есть хаскельный do с yield вместо return.

хотя аппликативного интерфейса тут достаточно:

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

То equality типов а не их элементов, кроме того, это экстенсиональная форма, например

struct bar;
strcut foo { char a; struct bar *x; };
strcut bar { long b; struct foo *y; }

foo <: bar, bar <: foo, foo = bar, но я предпочту выразить этот факт существованием биекции, оставив equality интенсиональным.

То equality типов а не их элементов

Ну да, а нам другого equality и не надо. Нафиг нам eqaulity элементов если результат объединения никак не зависит от значений принадлежащих типу и от их equality?

но я предпочту выразить этот факт существованием биекции, оставив equality интенсиональным.

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

Ну и да, вообще говоря, у нас все интересные типы будут равны друг другу, т.к. у них счетная мощность. Офигенно, наверное, когда A = List A = IO A и так далее? :)

Нафиг нам eqaulity элементов если результат объединения никак не зависит от значений принадлежащих типу и от их equality?

В смысле x : X, y : Y | x : X U Y and y : X U Y не зависит? «Shape» типа всё равно зависит от него — в зависимости от выбора x == y для разных значений можно будет наблюдать что количество различных значений в X U Y будет разным (их можно тупо посчитать, даже в самом языке). В этом же и суть — неразмеченное объединение отличается от размеченного пересечением в котором элементы разных типов отождествляются (по == для элементов), иначе (когда пересечение пусто) всегда бы была биекция между неразмеченными и размеченными.

Есть типы с биекцией, но не равные друг другу

Я об этом и говорю — интенсионально foo != bar, хотя можно доказать наличие биекции (пусть даже и в самом языке с помощью уже propositional equality).

Офигенно, наверное, когда A = List A = IO A и так далее? :)

Так это же ты хочешь считать биекцию за равенство.

кроме того, это экстенсиональная форма

Ну и кстати это как раз интенсиональная форма (не зависимая от элементов) а экстенсиональную ты предлагаешь.

Ну и IO это дерево.

а экстенсиональную ты предлагаешь

Я предлагаю интенсиональную — A == A, с точностью до синонимов. Всё. У тебя равенство типов предполагает нетривиальное доказательство A <: B, B <: A.

ну всё, теперь это тред Великого и Ужасного quasimoto и тяжело-атлетического CS

а значит, </thread> :)

Кстати, если вводить подтипирование как http://en.wikipedia.org/wiki/Subtyping#Coercions, то необходимо

IsInjection : {A B : Set} → (A → B) → Set
IsInjection f = ∀ {x y} → f x ≡ f y → x ≡ y

то есть самому подтипированию нужно extensional/propositional equality для элементов. Для TT как-то не видно других вариантов, кроме как с помощью coercions.

Так это же ты хочешь считать биекцию за равенство.

Я? Нет, я не хочу. Я за равенство считаю то, что за него считается: A = B <=> A < B && B < A

Я об этом и говорю — интенсионально foo != bar

Ну да, ведь они не подтипы друг друга. То есть foo !< bar, bar !< foo.

«Shape» типа всё равно зависит от него

Нет.

количество различных значений в X U Y будет разным

Но при чем тут это? Это ни как не связано с объединением. Если у нас есть некоторое множество, то количество различных элементов в нем зависит от выбора equal, значит потвоему множества нельзя однозначно определить. И никакого отношения к объединениям это не имеет.

В этом же и суть — неразмеченное объединение отличается от размеченного пересечением в котором элементы разных типов отождествляются

В этом же и суть — неразмеченное объединение отличается от размеченного пересечением в котором элементы разных типов отождествляются

С чего вдруг? неразмеченное объединение - sup в решетке типов, где тут что-то про элементы и их отождествление? Про пересечение тоже ничего нет - вполне возможно что оно и не определено, наличие sup не гарантирует наличия inf.

И вообще если sup есть, то он определен однозначно (т.к. если А и В sup, то A <= B, B <= A => A = B). Поэтому мне вообще не понятен смысл этой дискуссии. Ты придумал свою хуйню которая не имеет отношения ни к теории ни к реальности и продолжаешь эту хуйню повторять.

Я предлагаю интенсиональную — A == A, с точностью до синонимов.

Нет, ты как раз что-то про элементы говоришь.

Всё. У тебя равенство типов предполагает нетривиальное доказательство A <: B, B <: A.

Это не определение равенства, это свойство отношения <.

Кстати, если вводить подтипирование как http://en.wikipedia.org/wiki/Subtyping#Coercions, то необходимо

Это опять ты придумал. Подходит любое отображение, инъективность не требуется.

в таких тредах для полного счастья не хватает только Олега.

Я за равенство считаю то, что за него считается: A = B <=> A < B && B < A

Это не то же самое что биекция между A и B?

Ну да, ведь они не подтипы друг друга. То есть foo !< bar, bar !< foo.

Не поэтому — просто они определены как разные типы, поэтому не могут быть равны в def. смысле. Насчёт !< — есть инъекция из foo в bar и наоборот, везде на месте bar может использоваться foo и наоборот, foo агрегирует bar и наоборот — чем не <?

Но при чем тут это?

При том, что мне интересно чем конкретно будет тип, то есть какие у него канонические элементы, сколько их и т.п.

неразмеченное объединение - sup в решетке типов, где тут что-то про элементы и их отождествление?

Откуда я знаю? Решётку с её аксиомами ты постулировал.

Если взять, например, (Martin-Löf's) теорию типов с индуктивными типами — есть там такая решётка подтипирования? Какие-то публикации кроме как про coercions?

Нет, ты как раз что-то про элементы говоришь.

Я говорил про элементы, ты — про типы. Если говорить про типы — ничего кроме простейшей формы их синонимичного равенства (то что может дать identity type для типов) я не рассматриваю, за остальным — функции между типами, биекции между ними, на основе equality элементов и т.п., то есть эквивалентности и их доказательства, а не равенства (хотя дополнительными аксиомами эквивалентности интернализируются в равенства). Если говорить про элементы — да, нужно либо extensional, либо его propositional интернализация в языке.

Подходит любое отображение, инъективность не требуется.

Если подходит любое отображение, то все типы — подтипы unit type, так как для всех типов a существует отображение a -> unit, в виде \lambda (_ : a) -> (unit : unit).

Это не то же самое что биекция между A и B?

Между А и B не может быть никаких биекций. Это не множества.

Насчёт !< — есть инъекция из foo в bar и наоборот, везде на месте bar может использоваться foo и наоборот, foo агрегирует bar и наоборот — чем не <?

То что есть инъекция ничего не значит, т.к. они не являются подтипами друг друга. При чем тут вообще инъекция?

При том, что мне интересно чем конкретно будет тип, то есть какие у него канонические элементы, сколько их и т.п.

Ну так тебя хоть с объединениями хоть без по твоей теории количество элементов в _любом_ типе будет зависеть от equal. Если только их не 0 и не 1 - в этом случае их всегда 0 либо 1.

Откуда я знаю?

Ну а кто знает? Ты же начал завел речь про элементы и отождествление. Вот мне и интересно откуда взялся этот бред.

Решётку с её аксиомами ты постулировал.

А я то тут при чем? Это стандартные определения. Система типов с подтипированием - ЧУП, с объединениями - решетка. Если не ЧУП - то это не подтипирование. Если не решетка - то у тебя нету объединений.

Если взять, например, (Martin-Löf's) теорию типов с индуктивными типами — есть там такая решётка подтипирования?

Ее нигде нет, пока ты не определил отношение <= (не задал ЧУП). А когда ты задал ЧУП, то, в зависимости от того, хороший <= или плохой у тебя получится решетка или нет. Но это не зависит от equal или экстенсиональных условий - это зависит только от задания <=. Причем тривиальную решетку мы можем получить всегда, если у нас есть Top, объявляя A | B = Top forall A, B.

Я говорил про элементы, ты — про типы.

Ну да, о чем и речь. Вот мне и непонятно - откуда у тебя вылезли элементы, если речь про типы шла? При чем тут вообще элементы? То, что A < B нам ничего об их элементах, вообще говоря, не сообщает. И сообщать не может, потому что типы - НЕ множества. И нету разумного способа их со множествами отождествить (т.к. нельзя построить ни биекции ни даже инъекции типов во множества).

Если говорить про типы — ничего кроме простейшей формы их синонимичного равенства (то что может дать identity type для типов) я не рассматриваю

Замечательно. Я тоже.

за остальным — функции между типами, биекции между ними

Биекций между типами и функций между типами не бывает. Биекции и функции у множеств бывают. У типов - нет. Не надо путать типы и множества.

Если подходит любое отображение, то все типы — подтипы unit type, так как для всех типов a существует отображение a -> unit, в виде \lambda (_ : a) -> (unit : unit).

1. Никто тебе не гарантирует что у нас вообще есть Unit

2. Если есть - таки да, все так как ты сказал. А что тебя смущает?

И даже мой любимый пролог там более популярен, чем CL=)

Гитхаб считает qmake проекты (*.pro) и другую муть за Пролог, отсюда и популярность.

И даже мой любимый пролог там более популярен, чем CL=)

Говно очень популярно среди мух. Всем переходить на говно?

;; Это я не про Пролог, если что.

Ну и как её передать?