Человеческое метапрограммирование

Настолько через зад автогеном, что это всё равно, что не умеет. А если случай чуть сложнее, то ты сам признал, что там начинается АД И ПОГИБЕЛЬ (С)

Можно делать во всех случаях, когда понятно что делать. Ты просто не понимаешь о чем речь идет - во всех нетривиальных случаях такого экспанда (когда внешнее раскрытие зависит от внутреннего) по-просту непонятно какое поведение _должно_ быть. Специфицировать его можно. А вот вывести - нельзя.

К слову в н2 вообще нельзя раскрыть внешнюю форму в зависимости от внутренней. И наоборот (внутренную от внешней) - тоже нельзя. По крайней мере примера такого продемонстрировано не было.

Ссылку.

syntax arm

Есть. В Н2 распространение информации такое что лиспу и не синилось.

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

Там не только макрос А может повлиять на вложенный макрос Б и в обратную сторону. Причем одновременно.

Ну вот еще раз - ты прост оне опнимаешь о чем гвооришь. В данном случае получается бесконечная рекурсия.

Но и макрос Б может повлиять на макрос Е который вложен в макрос Д вызванный рядом с макросом А.

Ну ты продемонстрируй, а мы посомтрим.

Это банально удобно. Например, тот же yield return в C# так и работает.

Так это тривиальный случай.

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

Ты пример приведешь? где у тебя хоть КАКИЕ-НИБУДЬ зависимости раскручиваются. пока чот у тебя етсь захардкоженный алгоритм экспанда который позволяет захардкоженным образом передавать захардкоженную информацию. У тебя уже сколько просят показать как расширить эту систему (и передать информацию из внешнег омакроса внутреннему) - а ты нихуя показать не можешь.

Не сможет. Ибо он выведет сразу 3 подходящих типа и сообщит о неоднозначности.

у любого ооп-языка наличие нескольких типов для значения — это типичная ситуация

далее твой if назовем normal_if, мой — crazy_if

рассмотрим

var v1 = normal_if(bla_bla_bla) Grandson(2) else Grandson(3)
var v4 =  crazy_if(bla_bla_bla) Grandfather(5) else Grandson(6)

в обоих случаях (v1 и v4) имеем полностью одинаковые варианты типизации из трех типов: Grandfather, Father, Grandson (при условии, что это reference types, ну или как в с++ звездочки поставить надо)

да, напомни твою нотацию, у тебя Grandfather > Grandson или наоборот?

А иначе они не отлавливаются. Ты вообще видел размеры тестов у серьёзных компиляторов?

если ты мне предлагаешь делать юнит-тесты *такого же* размера для компилятора, написанного на Н2, то я наверно предпочту вместо него какой-нить простой препроцессор или просто свой любимый язык — тестов столько же

Да нет, вы немного не о том

я обычно на «ты» общаюсь

Да нет, вы немного не о том

о том

если у нас нет информации о типах, то набор имен лексически видимых переменных является ни чем иным, как типом данных окружения — точнее типом данных агрегата (aggregate) которым является окружение

пример:

global var a;
function f(var b, var c) {
  var d;
  function g(var e) {
  /// точка 1
  }
}  

в точке 1 типом данных окружения является тип

struct {
  var a;
  function f(var _1, var _2);
  var b;
  var c;
  var d;
  function g(var _3);
  var e;
}

или че-то похожее

В чем вы видите разницу?

Я согласился, что разницы нет (в той же агде 5 это сахар для таких sss...), тут дело в другом - я там написал достаточно. Это обычная логика - с S S S S S Z : Nat нам есть что делать, с q : S S S S S Z - нечего, мы толком не знаем что это (разве что написать id : 5 -> 5; id x = x), можно считать, что 5 это точка типа (множества) Nat, которая сама по себе не множество.

Это не сумма, а объединение.

Ну or это и есть сумма типов, на уровне термов сумма = объединение (тегированное, если что).

Проблема в следующем - как задать произвольную функциональную зависимость?

Так же как в типе обычной функции.

Напишите тип для yoba.

Причём это не top-level определение? Так как никакого define нет, есть let - yoba x body = ⟦ let $ x = 1 in $ body ⟧; yoba : {T : Set} → ⟪ Name Int ⟫ → ⟪ T ⟫ → ⟪ T ⟫ (или ⟪ Name Int ⟫ → ⟪ Expr T ⟫ → ⟪ Expr T ⟫).

Ну где реализация-то?

Там нужно дописать что-то вроде

class HFlatten tree l | tree -> l where hFlatten :: tree -> l
instance HFlatten HNil HNil where hFlatten _ = HNil
instance HFlatten (HBox t) (HBox t) where hFlatten = id
instance (HFlatten t l, Flatten t' l', HAppend l l' l'') => HFlatten (t, t') l'' where flatten (l, r) = hAppend (flatten l) (flatten r)

но использовать всё равно невозможно (как и всю hlist) - типы не выводятся.

Есть такой flatten, можно либо так:

data MyData = MyInteger Integer | MyString String | ...

myFlatten :: Tree MyData -> [MyData]
myFlatten = flatten

либо так:

myFlatten :: Tree Dynamic -> [Dynamic]
myFlatten = flatten

Я не знаю какое у вас определение программы. Для меня программа - это терм ЯП. Разные термы - разные программы.

Для меня программа это нечто что кроме своей функциональности (набора функций работающих с данными таких-то типов) имеет ещё как минимум _интерфейс_. Число 5 - терм языка, но явно не программа (хотя его можно его превратить в программу суть которой в печатании числа «5», показывании «<html><head>...</head><body>5</body></html>», отправлении слова 5 по сети по такому-то протоколу и т.п. - нужно добавить соответствующий интерфейс).

Да.

Ну например (app f pat) применяет любую функцию f и матчит относительно паттерна pat.

fun :: [T] -> ...
fun []       = ...                                          -- PM
fun [x]      | pred x = ...                                 -- PM + Guards
             | ...                
fun (x:y:zs) | x > n, pat <- x, y < m, pat <- y, ... = ...  -- PM + Guards + PM + Guards + PM + ...
             | pat <- act zs, ...                           --      Action PM + ...

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

Ну, а какая польза от N2? Там тоже предполагается ограничивать макросы правилами типизации.

Можно делать во всех случаях, когда понятно что делать. Ты просто не понимаешь о чем речь идет - во всех нетривиальных случаях такого экспанда (когда внешнее раскрытие зависит от внутреннего) по-просту непонятно какое поведение _должно_ быть. Специфицировать его можно. А вот вывести - нельзя.

А не приходило в голову, что это ты не понимаешь?

К слову в н2 вообще нельзя раскрыть внешнюю форму в зависимости от внутренней. И наоборот (внутренную от внешней) - тоже нельзя. По крайней мере примера такого продемонстрировано не было.

Очень предварительный черновик. http://www.rsdn.ru/article/nemerle/N2/N2-Project.rsdnml.xml#EWYAE

Надеюсь то, что тип коллекции может быть выведен как на основе информации снаружи, так и изнутри foreach объяснять не надо.

И это только один из вариантов.

Ну вот еще раз - ты прост оне опнимаешь о чем гвооришь. В данном случае получается бесконечная рекурсия.

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

macro A
{
  field1 = 1;
  field2 = field1 + B.field2;
}

macro B
{
  field1 = 1;
  field2 = field1 + A.field1;
}

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

Например, в такой последовательности. B.field1 A.field1 B.field2 A.field2 И она даже в таком примитивном случае не единственная.

Если в макре Б написать field2 = field1 + A.field2 то у нас действительно получится цикл. Но и тут в моем случае бесконечной рекурсии не будет. Вычислитель остановится, когда не будет готовых вычислений. Просто останется невычисленный кусок, о котором компилятор расскажет во всех подробностях.

HFlatten (t, t') l" where flatten (l, r) = hAppend (flatten l) (flatten r)

HFlatten (HCons t t') l" where flatten (HCons l r) = hAppend (flatten l) (flatten r)

у любого ооп-языка наличие нескольких типов для значения — это типичная ситуация

Чё? Статический тип всегда один.

в обоих случаях (v1 и v4) имеем полностью одинаковые варианты типизации из трех типов:

Разные. Ибо количество привидений типа имеет значение.

если ты мне предлагаешь делать юнит-тесты *такого же* размера для компилятора, написанного на Н2, то я наверно предпочту вместо него какой-нить простой препроцессор или просто свой любимый язык — тестов столько же

Для препроцессора тебе понадобится _БОЛЬШЕ_ тестов.

Для обычного языка на порядки больше, ибо у тебя кода будет на порядки больше.

в точке 1 типом данных окружения является тип

А, ну да. Но мы можем связать произвольную информацию с идентификатором, вот так:

global var a;
global syntax-var h = "any information"
function f(var b, var c) {
  var d;
  function g(var e) {
  /// точка 1
  }
}  

соответственно:

struct {
  var a;
  var f;
  var b;
  var c;
  var d;
  var g;
  var e;
  syntax-var h = any information"
}

q : S S S S S Z - нечего

Ну так чекер знает, что 5 - это S S S S S Z: Nat.

Ну or это и есть сумма типов, на уровне термов сумма = объединение

Сумма - это размеченное объединение. А мы говорим о неразмеченном.

Так же как в типе обычной функции.

Пример?

Причём это не top-level определение?

А почему оно должно быть тайплевел? Мы же можем определять локлаьные переменные? Можем.

Так как никакого define нет

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

но использовать всё равно невозможно (как и всю hlist) - типы не выводятся.

Ага. Нам типы-то надо знать в компайлтайме. А на практике мы их можем и не знать - какая конкретно вложенность будет известно только в рантайме. то есть flatten написать нельзя. Точнее можно - но в рамках хаскеля мы не сможем доказать его корректность. В том же Typed Racket тоже нельзя - можно только написать flatten с предикатом (то есть например flatten для списков произвольной вложенности Int'ов)

Для меня программа это нечто что кроме своей функциональности (набора функций работающих с данными таких-то типов) имеет ещё как минимум _интерфейс_. Число 5 - терм языка, но явно не программа (хотя его можно его превратить в программу суть которой в печатании числа «5», показывании «<html><head>...</head><body>5</body></html>», отправлении слова 5 по сети по такому-то протоколу и т.п. - нужно добавить соответствующий интерфейс).

То есть программа у тебя - это программа (общепринятое понимание) + вычислитель. В любом случае прошлые тезисы будут некорректны.

fun :: [T] -> ...

Ну так это не паттерн-матчинг - это руками-писательство. Никто же и не спорил что то же самое можно сделать и по-другому. Даже в брейнфаке.

Ну, а какая польза от N2? Там тоже предполагается ограничивать макросы правилами типизации.

Никакой. С того разговор и начался - я указал, что от системы метапрограммирования с типами пользы никакой нет.

А не приходило в голову, что это ты не понимаешь?

Так дело в том, что я в обсуждаемом предмете прекрансо разбираюсь, а ты - совсем никак. Кто, более вероятно, не понимает?

Очень предварительный черновик. http://www.rsdn.ru/article/nemerle/N2/N2-Project.rsdnml.xml#EWYAE

Ну и где там раскрытие внутреннего макроса в зависимости от раскрытия внешнего? Или какой-либо другйо пример?

Надеюсь то, что тип коллекции может быть выведен как на основе информации снаружи, так и изнутри foreach объяснять не надо.

Это ясно. Но будет ли продемонстрирова пример, как внутренний Б раскрывается в зависимости от внешнего А?

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

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

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

Так там есть последовательность вычисления - сперва вычисляется Б, потом А, так и только так. Причем макросы друг с другом не связаны в твоем случае - то есть никакая информация от макроса к макросу не идет, они работают с общей лексической информацией в точке раскрытия.

Давай рассмотрим вариант с циклическими связями, ты говорил, что они корректно разрешаются:

macro A
{
  field1 = 1;
  field2 = field1 + B.field2;
}

macro B
{
  field1 = 1;
  field2 = field1 + A.field2;
}

Если в макре Б написать field2 = field1 + A.field2 то у нас действительно получится цикл.

Охренеть, так твой вычислитель решает проблему останова? Это чудесно. Когда нобелевку получите? Или хост язык не тьюринг-полон?

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

Так дело в том, что я в обсуждаемом предмете прекрансо разбираюсь, а ты - совсем никак. Кто, более вероятно, не понимает?

У меня прямо противоположное мнение.

Ну и где там раскрытие внутреннего макроса в зависимости от раскрытия внешнего? Или какой-либо другйо пример?

Ох. Ты видишь как foreach по-разному раскрывается из-за того что тип коллекции получается другим?

Это ясно. Но будет ли продемонстрирова пример, как внутренний Б раскрывается в зависимости от внешнего А?

foreach (collection in collectionOfCollections)
  foreach (value in collection)
    ...

Этот код будет раскрываться сильно по-разному в зависимости от того какой тип имеет collectionOfCollections.

Причем вложенный foreach зависит от внешнего. Ибо использует переменную, которую создает внешний.

Если это не зависимость тогда я не понимаю что такое зависимость в твоем понимании.

Так там есть последовательность вычисления - сперва вычисляется Б, потом А, так и только так.

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

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

Как это не идет? А то, что у макросов есть публичные поля и они могут читать/писать свои и чужие поля это не обмен информацией?

Охренеть, так твой вычислитель решает проблему останова? Это чудесно. Когда нобелевку получите? Или хост язык не тьюринг-полон?

1)Вычислитель не мой.

2)Не решает. Тут её просто нет.

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

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

Все что произойдет это то, что вычислитель найдет цикл и остановится.

Вернее он вычислит всё кроме тех данных для вычисления, которых не хватает данных. Циклы частный случай.

После чего он сможет рассказать, какие именно данные не были вычислены.

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

Вот видишь. Если подумать, то проблема останова уже пропала... Вот только у меня система намного круче, чем простое реактивное программирование.

Хотя оно мне тоже понадобится. Но только для ИДЕ. Чтобы инкрементально обновлять информацию о коде. Иначе на многомегабайтных проектах всё очень печально получается.

Ну так чекер знает, что 5 - это S S S S S Z: Nat.

[повторяя -й раз] А про ? : S S S S S Z он ничего знать не может.

А мы говорим о неразмеченном.

Я говорю про размеченные. Неразмеченные могут ломать статическую систему типов - их, например, забанили в Cyclone (они там есть в ограниченном виде) и в Go (вообще). Не говоря уже про все ML-и.

Пример?

Определи что такое функциональная зависимость. Я думал ты говоришь про сигнатуры с зависимостью вида A -> T[A].

А почему оно должно быть тайплевел? Мы же можем определять локлаьные переменные? Можем.

Я так и понял - там пример для введения локальной переменной, такое и в нынешнем TH должно работать (только там нет параметризации Name / Expr типами и нет возможности подставлять цитированные Name и Expr независимо).

Можешь считать, что внутренние дефайны раскрываются в летрек-форму (собственно, это так и происходит). Так какой тип будет?

Это я там и написал. Можно потребовать ещё гарантии чтобы в letrec's body _обязательно_ использовалась вводимая переменная, т.е. body[name] и чтобы в типе это тоже отражалось, но это уже вообще - перегибать палку с типизацией. Чтобы сделать такую гарантию где-нибудь в CL придётся пройтись по body code-walkerом «до обратной кавычки».

то есть flatten написать нельзя.

Так flatten из пакета containers чем не подходит? У него параметрически-полиморфный тип Tree a -> [a], то есть у нас _есть_ гарантия, что с одной стороны - дерево, а с другой стороны - список. Причём дерево и список либо гомогенные от произвольных типов (в том числе размеченных объединений любых других нужных типов, но с обёртками-конструкторами, да), либо гетерогенные (от Dynamic, например).

В любом случае прошлые тезисы будут некорректны.

Я просто высказал своё удивление - я не вижу каких-то магических программ которые нельзя было бы написать в статике, но можно в динамике. Алгоритмы все те же самые, IO есть, сообщения и процессы есть, строго-нормализированному языку можно добавить fix / partiality monad.

Ну так это не паттерн-матчинг

А зачем цитировать тип? Тип тут ни при чём - это паттерн-матчинг как его понимают в ML-ях (и тех языках которые этот PM из ML-я заимствовали), то есть специальная форма case/match.

С того разговор и начался - я указал, что от системы метапрограммирования с типами пользы никакой нет.

То есть, задачи метапрограммирования настолько исключительные, что их нельзя свести к написанию статически типизированных функций (в том числе для типов вроде (Name T) и (Expr T)) которые будет использовать экпандер в своих переписываниях?

Ох. Ты видишь как foreach по-разному раскрывается из-за того что тип коллекции получается другим?

Вижу, а как теперь сделать, чтобы внутренний макрос раскрывался по-разному в зависимости от того, как раскрывается внешний? То, что ты сделал - на Racket будет вот так:

(define-syntax (for stx)  
  (syntax-parse stx
    [(for ([id:id (~var collection (static type1? #f))]) body ...) 
     #'(blah-blah-blah1)]
    [(for ([id:id (~var collection (static type2? #f))]) body ...) 
     #'(blah-blah-blah2)]))

Причем вложенный foreach зависит от внешнего. Ибо использует переменную, которую создает внешний.

Он не зависит от внешнего for, он зависит от переменной, которая находится в форме макровызова ВНУТРЕННЕГО for. То есть на внешний for внутренний for НИКАК НЕ ССЫЛАЕТСЯ. Можно вообще убрать внешний for, оставив переменную с тем же типом, которую он ввел - и раскрытие внутреннего for не изменится. Я просил нечто вроде этого:

> (define-syntax-parameter yoba
    (λ (stx) #'"pizda"))
> (define-syntax-rule (to-huy body ...) 
    (syntax-parameterize ([yoba (λ (stx) #'"huy")])
      body ...))
> (displayln (yoba))
pizda
> (to-huy (displayln (yoba)))
huy
> 

Как это не идет? А то, что у макросов есть публичные поля и они могут читать/писать свои и чужие поля это не обмен информацией?

Ну, видимо, тут возникло некое непонимание :( Вот такое «чтение полей» - нет, это не то, что я подразумевал под «обменом информацией, оно тривиально реализуется и вообще не заслуживает какого-либо обсуждения. Я боюсь, что экспанд в макросах слишком отличается даже по базовым принципам от твоей модели так что тут аналогий просто не подберешь. Проблема тут в том, что я могу выразить твою модель через обычный экспанд, а ты обычный экспанд выразить не сможешь - т.к. для обычного экспанда мы _должны_ зафиксировать порядок вычислений. То есть я могу создать у себя некую специальную „зону“ которая будет работать аналогично твоим типам (пожалуй, я даже напишу себе такую бибилотеку на будущее - в некоторых случаях подобный механизм действительно удобен, спасибо за идею) - не зависеть от порядка, разрешать зависимости автоматом и т.п., но ты аналогичную лисповому экспанду „зону“ (императивную) не реализуешь.

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

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

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

Я так полагаю, что топологическую сортировку ты-таки и делаешь перед началом работы алгоритма, нет? :)

Вот только у меня система намного круче, чем простое реактивное программирование.

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

[повторяя -й раз] А про ? : S S S S S Z он ничего знать не может.

Зачем нам знать про ? : S S S S S Z, если у нас нету никакого ? : S S S S S Z, есть только S S S S S Z: Nat? Я упорно не понимаю, что меняется от того, что мы определили для типа синоним.

Я говорю про размеченные.

А я в примере своем говорил о неразмеченных. (or A B) - это неразмеченное объединение типов A и B.

Определи что такое функциональная зависимость. Я думал ты говоришь про сигнатуры с зависимостью вида A -> T[A].

Ну давай пример, имеем такой тип (Expr (Type (or Integer String)) (Type (F A))), где F A = if (A = String) then Integer else (List Integer).

Я так и понял - там пример для введения локальной переменной, такое и в нынешнем TH должно работать

Только его в нынешнем TH нельзя типизировать (всмысле так чтобы чекнулся до экспанда). Давай пока остановимся на дефайне (для него тип проще, с let'ом там все сложнее, если для дефайна не напишешь - для let тем более не напишешь :)). Итак, какой тип у макроса (yoba x) -> (define yoba x)? Потом к let перейдем. а перейти надо обязательно т.к. от типизации макроса, раскрывающегося в let, мы перейдем к типизации макроса, раскрывающегося в лямбду, а этосамое нитеренсое :)

Это я там и написал.

Что написал? Каким образом указать в типе, что «здесь в лексическом контексте есть переменная, имеющая имя name и тип Type»? вернемся к макросу, раскрывшемуся в дефайн (будем от простого к сложному идти) - какой у него тип?

Можно потребовать ещё гарантии чтобы в letrec's body _обязательно_ использовалась вводимая переменная

Именно! Но только не можем, а должны! Ведь тип макроса говорит «макрос вводит переменную х». Значит в коде в который он раскрывается мы МОЖЕМ использовать х. Значит макрос обязан раскрытым кодом х ввести - то есть раскрыться в летрек, где есть х. Иначе получится тайпчек пропустит код, в котором используется х, когда х неопределена.

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

Написать - можно, чекнуть - нельзя. вот программа: (print (+ (read) (read))) можешь сделать так, чтобы она чекнулась в системе типов хаскеля?

Алгоритмы все те же самые, IO есть, сообщения и процессы есть, строго-нормализированному языку можно добавить fix / partiality monad.

Ну так тут дело не в том, просто для любой пограммы в динамике можно написать программу в статике, которая совершает те же самые сайд-эффекты. Но это будет ДРУГАЯ программа. Вот и все. А та программа, что в динамике была, в статике не чекнется.

А зачем цитировать тип?

Не понял, при чем тут тип? Какой тип?

То есть, задачи метапрограммирования настолько исключительные, что их нельзя свести к написанию статически типизированных функций (в том числе для типов вроде (Name T) и (Expr T)) которые будет использовать экпандер в своих переписываниях?

Почему нельзя? Я неточно выразился - _практической_ пользы никакой нет. То есть свести-то можно, но использовать такую систему на практике будет невоможно из-за того, что она неудобна. Так же как можно все задачи брейнфаком решать, но никто не решает - неудобно. Ты опять прыгаешь туда сюда между теоретической возможностью и практической целесообразностью. Информация о том, что в теории что-то МОЖНО совершенно бесполезно. Задача, которая решается за миллиард лет, на практике является неразрешимой.

[повторяя -й раз] А про ? : S S S S S Z он ничего знать не может.

А, понял что за проблема. Оставим S S S S Z. рассмотрим некоторый тип X, который имеет только одно значение (это значение будет нулем) и введем ф-я на уровне типов F. И припишем единице тип F X, двойке - F F X и так далее. Ну для удобства можешь взять X: Int (на самом деле требование, чтобы у типа было одно значение - не обязательно), а в качестве F - List. В данном случае натуральные числа кодируются списком соответствующей вложенности (на уровне значений).

Я неточно выразился - _практической_ пользы никакой нет.

В TH, F#, Nemerle есть элементы метапрограммирования которые используются - польза есть.

З.Ы. Я в wp://Metaprogramming ссылочку добавил.

Так flatten из пакета containers чем не подходит? У него параметрически-полиморфный тип Tree a -> [a]

Ну так это смовершенно другая функция, которая делает список из дерева. А я хочу функцию, которая делает список из списка списков ... списков :)

(define-type (Listof* A) (Rec T (U A (Listof T))))
(: flatten (All (A) ((Listof* A) ((Listof* A) -> Boolean : A) -> (Listof A))))

(define (flatten lst pred?)
  (let loop ([lst lst])
    (cond [(pred? lst)  (list lst)]  
          [else  (append* (map loop lst))])))

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

В TH, F#, Nemerle есть элементы метапрограммирования которые используются - польза есть.

Там нигде нету метапрограммирования, которое чекает макросы до экспанда.

Зависимость внешнего макроса от внутреннего заключается в том, что внешний макрос будет раскрыт так или иначе в зависимости от того, будет ли ГДЕ-ТО ВНУТРИ в том ли ином (в любом виде) раскрыт некий другой макрос и как он будет раскрыт.

На этапе типизации collect смотрит в текущий скоп. Если там есть for он добавляет себя в коллекцию вложенных в for макросов, которые работают с for. Если нет, то ругается пользователю красивым сообщением.

После чего они смогут спокойно поговорить.

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

syntax For is Expr
parsing "for" "(" ... ")" Body
{
  alias Body = Expr;
}
typing
{
  def Collects : Table[Collect];
  scope ForScope;
  type Body in ForScope;
}

syntax Collect is Expr
parsing "collect" Value ";"
{
  alias Value = Expr;
}
typing
{
  def owner = if in scope(For.ForScope as forScope)
    forScope.Owner;
  else
    error "not in for";
  owner.Collects.Add(this);
}

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

Очень смелое заявление, учитывая, что ты ничего не понял.

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

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

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

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

Если бы это было реактивное программирование, я бы так и сказал. Но ничего общего с реактивным программированием у меня нет.

Я так полагаю, что топологическую сортировку ты-таки и делаешь перед началом работы алгоритма, нет? :)

Не делаю. Вычислительный базис работает и без этого. Более того её сделать невозможно. Ибо новые узлы и связи появляются во время работы. Да и просто глядя на код нельзя сказать, куда пойдет вычисление. «Функция» len может у списка посчитать длину. Или из длины, сделать список. Пока не запустишь, не узнаешь. Сорвало крышу? Не понимаешь где она возьмет значение для списка? А нигде. Элементы списка не будут иметь значений, пока ты их туда не положишь. И при попытке чтения этих элементов атомарной операцией она просто остановится, пока кто-то не положит туда значение. После чего она снова станет готовой к выполнению. А с пользовательскими «функциями» все еще веселее. Они прочитают значение, и продолжат работу пока системная «функция» не наткнется на пустое значение. Причем даже если часть пользовательской «функции» заткнулась, другая часть продолжит работу. Вот такой весёлый вычислительный базис. И это только снежинки на верхушке айсберга.

На этапе типизации collect смотрит в текущий скоп. Если там есть for он добавляет себя в коллекцию вложенных в for макросов, которые работают с for. Если нет, то ругается пользователю красивым сообщением.

Откуда collect узнает о for, если макросы не раскрыты? Ну то есть мы имеем макрос (yoba body) -> (for ([id '(1 2)]) body) и вызываем (yoba (collect x)). Откуда внутренний collect знает на этапе типизации, что yoba раскроется в for (если типизация происходит до раскрытия)?

Очень смелое заявление, учитывая, что ты ничего не понял.

Я все прекрасно понял.

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

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

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

Чем он ограничивает? Еще раз - я могу повторить твой алгоритм через expand. Он прямо выражается.

Если бы это было реактивное программирование, я бы так и сказал. Но ничего общего с реактивным программированием у меня нет.

Тогда что у тебя есть?

Ибо новые узлы и связи появляются во время работы.

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

Сорвало крышу?

Не понял, от чего?

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

Пока что ты не написал ничего отличного от реактивного программирования.

И это только снежинки на верхушке айсберга.

Ну так каковы не верхушки? ИтаК, мы выяснили, что твой алгоритм имеет в основе своей вычислительную модель реактивного программирования (то что ты выше описывал - оно и есть). Теперь напиши отличия.

Да, кстати:

Language: typed/racket [custom].
> (: xor ((U 0 1) (U 0 1) -> (U 0 1)))
> (define (xor x y)
    (cond
      [(and (zero? y) (zero? x)) (+ x y)]
      [(or (zero? x) (zero? y)) 1]
      [else 0]))
> (xor 0 0)
- : Integer [generalized from (U Zero One)]
0
> (xor 0 1)
- : Integer [generalized from (U Zero One)]
1
> (xor 1 0)
- : Integer [generalized from (U Zero One)]
1
> (xor 1 1)
- : Integer [generalized from (U Zero One)]
0
> (xor 1 2)
. Type Checker: Expected (U Zero One), but got Positive-Byte in: 2
> 

И никаких проблем с типами 1 или 0 :)

А то, что агда слабовата и в ней такой не выразить - ну это проблемы агды.

Откуда collect узнает о for, если макросы не раскрыты? Ну то есть мы имеем макрос (yoba body) -> (for ([id '(1 2)]) body) и вызываем (yoba (collect x)). Откуда внутренний collect знает на этапе типизации, что yoba раскроется в for (если типизация происходит до раскрытия)?

Следует отметить - проблема осложняется тем, что макрос yoba может быть написан так, что мы вообще не сможем узнать раскроется ли он в for до того, как сформируем его АСТ. Ну например - он во время построения результирующего дерева читает некоторый файл и в зависимости от его содержимого раскрывается в for либо в другую форму. Соответственно, чтобы узнать, что там for - надо прочитать файл. Но на этапе тайпчека ты не можешь исполнять сайд-эффекты (как чтение файла, например ...).

И туда же о типизации макроса. В данном случае тип макроса будет содержать ссылку на то, что его АСТ формируется на основе информации из файла. Нифига себе тип, ну.

А я в примере своем говорил о неразмеченных.

Нету в языке.

(Expr (Type (or Integer String)) (Type (F A))), где F A = if (A = String) then Integer else (List Integer)

postulate
  foo : (T : U₀) → T ≡ ℤ₋ ⊎ T ≡ String₋ → if T ~ String₋ then ℤ₋ ⁺ else List (ℤ₋ ⁺)

bar₁ = foo String₋ (inj₂ refl)
-- C-c C-d bar₁ RET ⇒ ℤ

bar₂ = foo ℤ₋ (inj₁ refl)
-- C-c C-d bar₂ RET ⇒ List ℤ

(disclaimer: U₀ это синтетический универсум, но это проблемы агды) больше ничего не пишется, потому что только эти два свидетельства (inj₁ refl и inj₂ refl) можно передать.

Но только не можем, а должны

То есть что-то вроде

postulate
  -- type (: U(0), U(1), ...) quoting
  ⟪_⟫ : ∀ {l} → Set l → Set l
  -- term (: T, U(0), U(1), ...) quoting
  ⟦_⟧ : ∀ {l} {T : Set l} → T → ⟪ T ⟫
  -- term splicing
  $_ : ∀ {l} {T : Set l} → ⟪ T ⟫ → T
  -- any type
  Dynamic : Set
  -- dynamic term splicing (for heterogeneous lists)
  $$_ : ∀ {l} {T : Set l} → ⟪ T ⟫ → Dynamic
  -- named thing, parametrized by types
  Name : ∀ {l} → Set l → Set l
  -- expression, parametrized by scoped names and by type
  Expr[_]_ : ∀ {l} → List Dynamic → Set l → Set l

  example : (name₁ : ⟪ Name ℤ ⟫) → (name₂ : ⟪ Name String ⟫) → ⟪ Expr[ $$ name₁ ∷ $$ name₂ ∷ [] ] ⊤ ⟫

тут две вводимых переменных разных типов, тип выражения параметризован именами скопа и результирующим типом (тут ⊤ так как define ничего не возвращает, ЕМНИП).

(print (+ (read) (read)))

read + read, где read = Prelude.read <$> getLine и (+) = liftM2 (Prelude.+).

Какой тип?

Ты процитировал тип fun и сказал «это не паттерн-матчинг». Почему нет?

А я хочу функцию, которая делает список из списка списков ... списков :)

Это какие-то рэкето-заморочки - придумывать типы для «списка списков». Вообще это называется дерево (хорошо, что ты не спрашиваешь про cons-пары :)).

Там нигде нету метапрограммирования, которое чекает макросы до экспанда.

В TH есть (но очень примитивное, хотя об этом известно). В MetaML/MetaOCaml есть (получше, как говорят - я их не смотрел).

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

Да нет - это обычный лисповый flatten. Просто пример функции, корректность которой нельзя доказать в том же хаскеле, но можно - в Typed Racket. Видишь ли в чем дело - спецификации пишутся _вне_ системы типов. И корректность программы надо доказывать на соответствие этим спецификациям. В качестве типа у нас может выступать любой предикат, то есть спецификация может быть такая: «написать программу, которая суммирует тройку чисел, не удовлетворяющих Великой Теореме Ферма». Мы, конечно, можем взять просто f x y z = x + y + z. Она все числа суммирует и те что нужны - суммирует тем более. Но программа f x y z = any тоже будет правильной. Однако, ее корректность доказать несколько затруднительно ;)

Так и тут - нужна ф-я, которая принимает списков списков любой вложенности и возвращает обычный список. То, что в какой-то системе типов нету рекурсивных типов с объединениями - проблема этой системы :)

В TH есть (но очень примитивное, хотя об этом известно).

Давай определимся. Здесь и далее под «тайпчеком макросов» понимается такой тайпчек макроса, который позволяет не чекать раскрытый код. То есть позволяет гарантировать корректность программы до начала экспанда.

Это частичная функция, должно быть

_⨁_ : Bool → Bool → Bool
true ⨁ true  = false
false ⨁ true  = true
true ⨁ false = true
false ⨁ false = false

в крайнем случае

xor : (m n : ℕ) → (m ≡ 0 ⊎ m ≡ 1) × (n ≡ 0 ⊎ n ≡ 1) → Maybe ℕ

но тут нет ограничений на ОДЗ и свидетельство нужно передать, так что не нужно.

А в рэкете это ведь просто контракт? ДСЛ для задания assert-like проверок внутри функции - что будет делать (compile-time) чекер с (xor (read) (read))?

А то, что агда слабовата и в ней такой не выразить - ну это проблемы агды.

Агда непротиворечива и правильна, поэтому может применяться в той узкой области для которой она создавалась. В отличии от.

Здесь и далее под «тайпчеком макросов» понимается такой тайпчек макроса, который позволяет не чекать раскрытый код.

Да, в этом треде были примеры выхлопа тайпчекера для «до экспанда». Просто это практически мало применимо пока Expr не будет параметризирован (в треде есть и ссылка на proposal), но чисто как машинерия - тайпчек до экспанда в TH уже работает просто как обычный тайпчек.

Ты процитировал тип fun и сказал «это не паттерн-матчинг». Почему нет?

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

Нету в языке.

А мы говорили разве о каком-то _конкретном_ языке? Не припомню такого. В моем во тесть. И что делать? :)

Вообще такие объединения в языке, который разбирает и генерирует АСТ обязаны быть. Иначе никаких интересных (несводимых к лени) макросов ты не напишешь.

больше ничего не пишется, потому что только эти два свидетельства (inj₁ refl и inj₂ refl) можно передать.

Ну вот, прекрасно. Теперь представим, что макрос раскрывается так: (f x) -> if (list? x) then int->str $ (car x) else x, тип у него такой f: T -> (Expr (Type String)), где Т - это тот тип с зависимостью, что ты указал. Сможешь доказать корректность макроса? То есть тот факт что он действительно вернет string?

тут две вводимых переменных разных типов, тип выражения параметризован именами скопа и результирующим типом (тут ⊤ так как define ничего не возвращает, ЕМНИП).

Теперь вернемся к примеру с let, но сразу перепишем его в пример с лямбдой: Допустим, макрос раскрывается так: (yoba (x ...) body) = (lambda (x ...) body). Количество переменных заранее неизвестно, конечно же. Теперь нам надо припиисать body типа, в котором будет указано что в лексическом контексте, где body будет чекаться, есть переменные х ... с соответтсвующими типами. И, бтв, не мог бы ты вместо квадратиков сделать какой-нибудь другой значок? как-нибудь так #(lalala) например? А то в глазах рябит.

Да, в этом треде были примеры выхлопа тайпчекера для «до экспанда».

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

Это частичная функция

Это тотальная функция.

должно быть

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

но тут нет ограничений на ОДЗ

Здесь переменные имеют тип Nat, а должны - Bool = (U 0 1). Так что не пойдет.

А в рэкете это ведь просто контракт?

Нет, коненчо. Там же написано было (когда пршло не 0 и не 1) - ошибка тайпчека :)

Чекер проверяет, пришло ли на вход 0/1 и выдает ошибку, если пришло что-то другое (во время тайпчека). Если же все пришло ок - то чекер гарантирует, что возвращаемое значение имеет тип (U 0 1). Собсно там как ты видел был (+ x y), так вот это дело чекнулось лишь потому, что тайпчекер вывел из (and (zero? x) (zero? y)), что типы x/y в этой ветке будут 0 (это occurence typing - то есть тип сужается на основе информации в коде). А значит тип возвращаемого значения - тоже 0, то есть чек корректный. Если бы чекер не смог вывести что у имеет тип 0, а имеет тип Integer, например, то (+ x y) имело бы тип Integer, а не 0, и была бы ошибка тайпчека. Так-то! :)

Агда непротиворечива и правильна, поэтому может применяться в той узкой области для которой она создавалась. В отличии от.

Racket тоже непротиворечив и правилен, поэтому может применяться в узкой области, для котрой создавался :)

Можно вообще обойтись и обычными if'ами при желании.

Сложный паттерн в одну строчку с кучей вложенных конструкторов, биндингов и прочерков легко превращается в эквивалентную лапшу if-let цепочек на десятки строк.

А мы говорили разве о каком-то _конкретном_ языке?

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

(f x) -> if (list? x) then int->str $ (car x) else x, тип у него такой f: T -> (Expr (Type String))

Вот это я не понял. Тип T (то что принимает f) это (число или строка)? Или (число или список чисел), то есть результат (F T)? Что такое «int->str $ (car x)»?

И, бтв, не мог бы ты вместо квадратиков сделать какой-нибудь другой значок?

Каких квадратиков?

Здесь переменные имеют тип Nat, а должны - Bool = (U 0 1).

Тогда первый вариант с Bool - как раз оно. Может (U 0 1) там интерпретируется как пара nullарных конструкторов по написанию совпадающих с числами 0 и 1 - автоматически поднимается индуктивный тип Bool : Type; 0_con : Bool; 1_con : Bool именно для этой функции, но семантически всё как для функции Bool → Bool → Bool. Ну сахар, чо.

Так-то!

Ээ, так как он собирается чекать (xor (read) (read)) если это тотальная функция и проверка времени компиляции?

Racket тоже непротиворечив и правилен, поэтому может применяться в узкой области, для котрой создавался :)

Consistency and soundness. Агда хороша не сама по себе - хороша метатеория MLTT. У Racket нет основания.

Видишь ли в чем дело - спецификации пишутся _вне_ системы типов.

Да, спецификация может быть невыразима (объективно или субъективно) в рамках такой-то системы типов, но как-то верификацию всё равно делать нужно (пусть даже покрывать тестами, хотя это не совсем верификация).

нужна ф-я, которая принимает списков списков любой вложенности

Я просто не знаю такого типа, я знаю тип «список элементов такого-то типа» или «список элементов такого-то типа такой-то длины» (вот бы в С++ иметь vector<int, 5>), «дерево элементов такого-то типа» или «дерево элементов такого-то типа такой-то глубины» (tree<int, 5>?). Типов «список» и «дерево», по-хорошему, тоже нет^W^W я тоже не знаю - это будут списки и деревья для top type.

не чекать раскрытый код

Он чекает и сначала и потом. Где гарантия, что раскрытый код всегда корректен?

Каких квадратиков?

В примере твоего кода ты когда определяешь новую операцию у меня это выглядит как квадратик :cry: видимо, у меня со шрифтами проблема :)

Сложный паттерн в одну строчку с кучей вложенных конструкторов, биндингов и прочерков легко превращается в эквивалентную лапшу if-let цепочек на десятки строк.

Угу. По-этому чем выразительнее match - тем лучше экономися на if-ах :) В racket можно через паттерны вообще все что угодно вычислить, ну например - факториал :)

По крайней мере про безопасную статику.

Ок, с чего ты взял что в безопасной статике нету объединений?

Вот это я не понял. Тип T (то что принимает f) это (число или строка)? Или (число или список чисел), то есть результат (F T)?

Результат F. И вообще говоря это не число/строка, а цитата которая вернет число или цитата, которая вернет строку.

Что такое «int->str $ (car x)»?

Берем глову списка (у нас там число) и преобразуем его в строку.Ну то есть в любом случае макрос раскроется в выражение, возвращающее строку.

Где гарантия, что раскрытый код всегда корректен?

Так мы и обсуждаем такой тайпчек, который нам даст эту гарантию. Другой тайпчек (как в TH) не рассматриваем..

Consistency and soundness.

Именно, такая система типов в Racket и есть :)

У Racket нет основания.

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

Тогда первый вариант с Bool - как раз оно.

Нет, не оно. Мне нужен тип, у которого есть два значения - 0 и 1 и эти значения _числа_.

Может (U 0 1) там интерпретируется как пара nullарных конструкторов по написанию совпадающих с числами 0 и 1

Нет не интерпретируется. Это именно числа. Иначе каким бы образом я к этим конструкторам применил операцию +?

но семантически всё как для функции Bool → Bool → Bool. Ну сахар, чо.

Ну определи мне через Bool'ы с +, как у меня :) это именно числа. 0 э то тип, которому принадлежит одно значение, число 0. 1 - тип, которому принадлежит одно значени - число 1. (U 0 1) - тип, которому принадлежит два значения. Нутыпонелда.

Ээ, так как он собирается чекать (xor (read) (read)) если это тотальная функция и проверка времени компиляции?

Чекер поступит так, как поступает любой чекер - если корректность доказать невозможно, то выдается ошибка тайпчека. К слову, написанная тобой программа вообще некорректна с точки зрения типов, т.к. + принимает число, а read может вернуть что угодно. Надо так: (let ([x (read)] [y (read)]) (when (and (number? x) (number? y)) (+ x y)))

видимо, у меня со шрифтами проблема

Не знаю - в редакторе UTF-8, у ЛОРа тоже. Я потом над теми примерами подумаю.

В racket можно через паттерны вообще все что угодно вычислить, ну например - факториал

Если третий элемент списка больше чем факториал пяти, то сматчить его с заявленным именем, если меньше и по местному времени полночь +-30 минут - с именем составленным из заявленного и из первых трёх знаков дробной части числа пи. В CL тоже так можно.

Ок, с чего ты взял что в безопасной статике нету объединений?

ML-и (OCaml, SML, Haskell, F#, Nemerle (условно)), go, си небезопасен, в Cyclone ограничили неразмеченные ввели размеченные (и MLевский PM). Я ничего не путаю?

Я просто не знаю такого типа

Как все поразительно у типо-теоретиков - как только теория выходит за рамки их узкого мирка, так они сразу «не знаю». Ну что значит не знаю? Всмысле этот тип неопределим в некоей системе? Ну да. Для его определения нужны рекурсивные типы с объединениями. Это корректный и осмысленный тип. Множество его значений определяется следующим образом: x in A => x in (listof* A), x in (Listof (Listof A)) => x in (Listof* A). Вообще мы для _любого_ предиката можем построить тип из элементов, для которых этот предикат true. Собственно наиболее развитые и выразительные системы типов основаны именно на этом подходе (тип есть множество, то есть предикат). Кстати, в метатеории агды ЕСТЬ этот тип.

Если третий элемент списка больше чем факториал пяти, то сматчить его с заявленным именем, если меньше и по местному времени полночь +-30 минут - с именем составленным из заявленного и из первых трёх знаков дробной части числа пи.

А в хаскеле - нет :(

ML-и (OCaml, SML, Haskell, F#, Nemerle (условно)), go, си небезопасен, в Cyclone ограничили неразмеченные ввели размеченные (и MLевский PM). Я ничего не путаю?

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

Именно, такая система типов в Racket и есть :)

А пруфы есть? Бумажки какие-нибудь?

Мне нужен тип, у которого есть два значения - 0 и 1 и эти значения _числа_.

Изоморфизм же Bool ≅ ℕ (надеюсь, квадратиков нет), пусть это будут false и true с возможностью конвертации туда (но не обратно), даже автоматически - видим true + false, ищем в иерархии (с точки зрения сабтайпинга) путь Bool -> Nat (довольно короткий) и конвертируем.

Ну определи мне через Bool'ы с +, как у меня

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

(let ([x (read)] [y (read)]) (when (and (number? x) (number? y)) (+ x y)))

И если в stdin пришло 2 и 3 - как чекер это предскажет? Тогда получается частичная функция или по крайней мере сбой статических гарантий чекера. Тут должен быть какой-то каст (специальная форма) который может падать и обрабатываться.

А в хаскеле - нет :(

Это фича.

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

union t {
  // ...
  char *s;
  // ...
};

    union t x = { 0 };
    puts(x.s);

или это «проблемы негров»?

А пруфы есть? Бумажки какие-нибудь?

Погугли публикации. Ее не методом тыка делали.

Изоморфизм же Bool ≅ ℕ (надеюсь, квадратиков нет), пусть это будут false и true с возможностью конвертации туда (но не обратно), даже автоматически - видим true + false, ищем в иерархии (с точки зрения сабтайпинга) путь Bool -> Nat (довольно короткий) и конвертируем.

Ну вот видишь - ты сам придумал как сделать такие типы, чего же тогда мозги ебал хз сколько? :)

Но в typed racket никаких конвертаций нету - там любому значению соответстует тип, который содержит только это значение и никаких других. Вот и все. Так что этот bool - это именно не bool, а тип состоящий из двух числе. Я мог бы взять вместо них 3213 и 7658 например, а не 0 и 1.

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

Ну да в racket они и перегружены. толькоо не для булевых значений, а для 0 и 1. Можно перегрузить для 2, 3 , 4 ... :)

И если в stdin пришло 2 и 3 - как чекер это предскажет?

не понял почему он должен это предскзаать? Там же number. Зачем нам 2 или 3?

Тогда получается частичная функция или по крайней мере сбой статических гарантий чекера.

Нет, ни того ни другого не будет. С чего бы вдруг?

Это фича.

Странная фича :(

или это «проблемы негров»?

Еще раз, вопрос был следующим - почему статика с объединениями небезопасна? Я не просил приводить пример небезопасной статики с объединениями. И безопасной без них тоже не просил. Вопрос был другой, еще раз - ПОЧЕМУ СТАТИКА С ОБЪЕДИНЕНИЯМИ НЕ МОЖЕТ БЫТЬ БЕЗОПАСНОЙ? Доказывтаь надо не на примерах, а в общем. Для любого ЯП.

То есть передо мной вот Typed Racket - пример безопасной статики с объединениями, данный мне в ощущениях. И ты тут говоришь, что на самом деле Typed Racket не существует? Или как?