LINUX.ORG.RU

Man or boy 2к25: Ваш статически типизированный ЯП полноценен?

 


0

4

Когда то Кнут придумал тест для ALGOL реализаций, и он известен под именем «Man or boy test». Но там просто локальные функции, не особо интересно.

Предоставляю вам версию для проверки языка программирования, на то, достоен ли он существовать в 21 веке!

Для начала нарушу это правило (у Python динамическая типизация), и покажу Python версию:

def print_sum(x):
  def make(acc):
    def f(y):
      print("acc(%d) + %d" % (acc, y))
      return make (acc + y)
    return f
  return make(x)

print_sum(10)(20)(30)(40)
Вывод
acc(10) + 20
acc(30) + 30
acc(60) + 40

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

Мое повторение на OCaml с rectypes:

let print_sum x =
  let rec f acc = fun y ->
    printf "acc(%d) + %d\n" acc y;
    f (acc + y)
  in 
  f x
  
let () = ignore (print_sum 10 20 30 40)
Типы он вывел сам, но можно и указать вручную:
type t = int -> t 

let print_sum (x : int) : t =
  let rec f (acc : int) : t = fun (y : int) : t ->
    printf "acc(%d) + %d\n" acc y;
    f (acc + y)
  in 
  f x
  
let () = ignore (print_sum 10 20 30 40)

Языки которые смогли реализовать тест на лямбдах/функциях, их система типов и ее записи позволяет строить рекурсивные по возврату лямбды и функции:

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

Языки у которых пока не получилось без дополнительных средств типа классов/структур для обхода проблем с типами:

  • Rust (использование trait)
  • C (некорректная реализация)
  • Zig (использование классов)
  • D (использование делегатов)

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

★★★★★

Последнее исправление: MOPKOBKA (всего исправлений: 21)
Ответ на: комментарий от monk

Поэтому я и пишу, что вопрос в длине конвейера и буфера декодирования.

я вот не пишу код, настолько заточенный под «длину конвейера». Код просто должен нормально читаться и быстро работать, вне зависимости от длины конвейера проца, на котором его пустят. Может там и конвейера не будет. Может там и надписи Intel/AMD не будет.

alysnix ★★★
()
Ответ на: комментарий от alysnix

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

Если задача, написать самый короткий код, тогда, конечно, таблица.

monk ★★★★★
()
Ответ на: комментарий от alysnix

Может там и конвейера не будет. Может там и надписи Intel/AMD не будет.

Тогда лучше писать через switch и положиться на оптимизацию компилятора.

На Эльбрусе, кстати, вариант через таблицу ещё медленнее относительно переходов по условиям работает.

monk ★★★★★
()
Ответ на: комментарий от monk

Тогда лучше писать через switch и положиться на оптимизацию компилятора.

кому лучше? а если там 30 фигур и 900 сочетаний? вы предлагаете решение, работающее только в примитивных случаях.

alysnix ★★★
()
Ответ на: комментарий от alysnix

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

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

monk ★★★★★
()
Ответ на: комментарий от monk

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

Коллайдер будет строить коллекцию, и зарегив все фигуры, будет аллокировать таблицу правильного размера и заполнять функциями. число функций будет n*(n-1)/2, где n - число фигур, поскольку функции коммутативны.

не надо ручками править ваши кейзы. это ж прошлый век какой-то.

alysnix ★★★
()
Ответ на: комментарий от alysnix

если там 30 фигур и 900 сочетаний?

Можно заметить, что любая фигура — это полигон, и требуется только одна функция — для определения пересечения полигонов.

Никакого ооп-шмооп, никаких коллайдеров-шмайдеров не нужно.

Nervous ★★★★★
()
Последнее исправление: Nervous (всего исправлений: 1)
Ответ на: комментарий от Nervous

Это я уже высказывал на самом старте обсуждения. но Морковкин хотел макнуть и ООП и меня в сточную канаву и настаивал на именно такой, изощренной форме расчетов.

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

alysnix ★★★
()
Ответ на: комментарий от Nervous

Можно заметить, что любая фигура — это полигон, и требуется только одна функция — для определения пересечения полигонов.

Круг не является полигоном, эллипс не является полигоном. И ещё множество фигур.

monk ★★★★★
()
Ответ на: комментарий от monk

Круг не является полигоном, эллипс не является полигоном

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

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

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

Nervous ★★★★★
()
Последнее исправление: Nervous (всего исправлений: 1)
Ответ на: комментарий от Nervous

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

Можно. И задача, которая решалась на ЕС1841, внезапно начинает требовать видеокарту NVidia Quadro.

monk ★★★★★
()
Последнее исправление: monk (всего исправлений: 1)
Ответ на: комментарий от monk

Круг не является полигоном, эллипс не является полигоном. И ещё множество фигур.

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

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

Это есть основная парадигма ООП.

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

anonymous
()
Ответ на: комментарий от alysnix

естессно ООП легко справился с этой задачей

Сначала придумали себе (игрушечную) проблему, потом её доблестно решили. Молодцы %)

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

Nervous ★★★★★
()
Последнее исправление: Nervous (всего исправлений: 1)
Ответ на: комментарий от kaldeon

Шото той ChatGPT тут намудрил. Вот упрощённый вариант:

package main

import "fmt"

type fn func(int) fn

func printsum(acc int) fn {
	return func(x int) fn {
		fmt.Printf("acc(%d) + %d\n", acc, x)
		return printsum(acc + x)
	}
}

func main() {
	printsum(10)(20)(30)(40)
}
beastie ★★★★★
()
Ответ на: комментарий от alysnix

Упростить разработку.

Например у меня имеется алгоритм, которому на вход можно подать набор файлов какого-либо документа Microsoft Office,
Алгоритм проанализирует файлы и создаст метаданные, для подсистемы управления объектами в которой имеется возможность загрузки данных
из файла в днамически создаваемый объект.

Так это не фантазия, а реализовано и проверено.
Это был пример, когда подсистема управления объектами весьма упрощает разработку и тем самым экономит массу времени.

anonymous
()
Ответ на: комментарий от alysnix

Пожалуйста.
Скажем хотим сохранять состояния N диалоговых форм и восстанавливать его при открытии формы.
Можно для каждой формы создать свой xml, а можно много проще.
Кстати это не фантазия.

anonymous
()
Ответ на: комментарий от anonymous

Вот ещё неплохой пример пользы от системы управления объектами.
Это работа с xml.
У меня так, для любого xml можно автоматически создать мета данные.
Далее подсистема может данные этого xml загрузить в динамический объект и при этом значения будут в объекте в нативнов формате, а не текстовом.
Хотя ранее разработал API для работы с xml, но ныне его не использую.
Почему?
Подcистема управления динамическими объектами пригодная для работы
с объектами любой сложности.
Экономится масса времени и код много проще.

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

anonymous
()
Ответ на: комментарий от anonymous

В OСaml нету перегрузки, и я посчитал что нету способа рассмотреть тип после его перехода в функцию. Но сегодня я понял что через вывод типов можно его все же проверить его:

(* REPL *)

(* auto f(auto x) { return [](){return x;}; } *)
>>> let f x = fun () -> x;;
val f : 'a -> unit -> 'a = <fun>

>>> f 10;;
- : unit -> int = <fun>

>>> f "hello";;
- : unit -> string = <fun>

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

MOPKOBKA ★★★★★
() автор топика
Последнее исправление: MOPKOBKA (всего исправлений: 1)
Ответ на: комментарий от MOPKOBKA

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

При парсинге создаются метаданные с которые могу в run-time использовать (это одна из возможностей подсистемы работы с динамическими объектами).

Почему чвстенько пишу о своих разработках?

Чтобы другие не программировали «по понятиям», а решали «хотелки»
ныне не ожидая какой-то там манны когда-то от каких то стандартов.

anonymous
()
Ответ на: комментарий от MOPKOBKA

Но сегодня я понял что через вывод типов можно его все же проверить его:

Нельзя. Системы типов всех языков настолько немощные, что само понятие «тип» там не применимо.

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

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

Стирается. Это свойство любой рядовой типовой модели. Людей часто путает то, что когда-то в генерики была добавлена часть семантики цпп. Это даёт немного фокусов, но совсем немного.

val f : 'a -> unit -> 'a = <fun>

Это не вывод. Это простое правило «приравняй вход в выходу». Оно не понимает что это такое. Что такое типы.

>> f 10;;
- : unit -> int = <fun>

Он редуцирует твою сигнатуру до in=out и в текущем контексте тебе даёт «вывод». Это то самое «стащеное». Это только один из механизмов. Да, они научились запускать что-то на каждый вызов, но запускать «что-то» это не «запускать полезное».

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

Ты видишь auto -> auto и тебе кажется, что это T -> T - это одно и то же. В реальности, повторяю, это две отдельные записи. Она не имеет отношения к функции/сигнатуре/прочему. Это просто сахарок для заполнения таблиц.

Смотри. Код как-то преобразует входы в выходы. Он делает это в рантайме, а в рамках вывода типов у тебя есть такие же преобразования, но уже на уровне условной системы типов. И то и то вычисления просто разного уровня. Участвуют одинаковые конструкции.

И это фундаментальное свойство. (auto -> auto) говорит «тип является результатов преобразований написанных в теле», а ('a -> 'a) говорит «не имею никакого отношения к телу и вычислениям - я просто переопределяю логику вывода». А то, что ты называешь «выводом» это просто колхозный алгоритм, который пытается заполнить эти таблицы за тебя. Но их природы это не меняет. Да и работает это потому что язык и его система типов максимально примитивны. Как и логика на этих языках написанная.

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

Вот пример: https://gcc.godbolt.org/z/qaKnYfe6d

auto expr = [](auto a, auto b, auto c) { return (a + b + c) * c + b * a; };

auto wexpr = [](auto a, auto b, auto c) { return add(mul(add(add(a, b), c), c), mul(b, a)); };

Собственно в этом смысл вывода - его поведение определяется тем что ты написал в теле, а не тем что ты написал руками в виде 'a -> 'a.

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

Давай ещё раз как можно проще. Настоящий вывод идёт и рекурсивно вычисляет твоё выражение в теле функции в типовом контексте. Это некий новй слой вычислений. Поэтому он может воспроизводить семантику вычислений в рамках типов - отображая её. Допустим как в примере выше с арифметикой.

Нет смысла в выводе/тапах/прочего если ты не можешь это объединять друг с другом. Как ты можешь это делать в языке с выражениями обычными.

anonymous
()
Ответ на: комментарий от MOPKOBKA

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

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

id - это понятно. Там t->t, но что дальше? Ещё раз просто пойми что если что-то похоже это не значит что оно этим является. Ты написал 2 раза одно и тоже. В языке с выводом я написал это один раз. Пока там пол строчки тебе кажется что «ну разницы особой нет», а когда там будет программа целиком - ты напишешь её два раза. На самом деле ты никогда этого не напишешь потому как таблица не может обладать этими свойствами.

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

Аналогично когда ты видишь (auto a, auto b) -> decltype(std::tuple_cat(a, std::tuple{b})) - это совершенно не тоже самое что в допотопных языках. Понятно, что в данном случае есть какие-то сложны выражения, а что такое деклтайп - это просто инопланетные технологии для тех кто сидит на огрызках идустрии 80. Могут быть примеры проще и там может казаться, что «это похоже», но нет.

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

Дремучая теория пытается вводить всякие порядки. Будь то вывода/полиморфизма. И то, что для них где-то высоко в цпп это низко. Соответственно в цпп не просто есть вывод, а вывод как то что можешь использовать как обычную чиселку в твоей скриптухе. Это то, что у вас называется первым классом. Аналогично даже само существование вывода является первым классом.

Вот концепты и пример выше работают на этом уровне. Это даже не то что аналога нет - это даже у людей в рамках общих представлений не существует.

Аналогично и с типами. В дремучих языках типы даже не являются сущностями первого класса. Не говоря уже о чём-то построенном поверх них.

anonymous
()
Ответ на: комментарий от qulinxao3

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

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

Эти языки из полеолита примитивные по-сути водятся к банальному a -> b -> c аналогично сюда же сводится примитивная рекурсия, которая на самом деле не рекурсия. x=y - это id, x = f(y) - это id/out = m[it], генерики через одно место туда прикреченные это просто подъём этого m чтобы они писали рукой.

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

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

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

И вот у нас остаётся выбор - мы ограничивает язык до уровня неюзабельности и показываем неофитам фокусы, либо делаем его рабочим и тогда фокусы не работают. Индустрия шла и идёт по второму пути. А цирк он был и остался цирком.

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

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

Всегда можно сделать примитивно. Когдаэто это может работать. И вопрос в том что как сделать так чтобы это примитивно работало только тогда, когда это действительно имеет смысл. Ценность «давайте всё сведём к примитиву» отрицательная. Это можно сделать в цирке, но не в реальности. Повторяю.

anonymous
()
Ответ на: комментарий от anonymous

Конечно, твой окамл не настолько допотопное позорище как раст

Если верить википедии, то ML это 1973 год, так что вполне допотопный. Просто разное качество допотопности.

... ты написал руками в виде 'a -> 'a ...
... Ты написал 2 раза одно и тоже ...

Заметь что руками я написал только вот эти строки:

let f x = fun () -> x
f 10
f "hello"
А остальное уже выдает как вывод мне REPL.

Собственно в этом смысл вывода - его поведение определяется тем что ты написал в теле

Пример с выражениями повторить невозможно из за отсутствия перегрузки, но про операцию над типами в теле я подумаю (хотя бы про реализацию с одним int_t), позже напишу если будут вопросы.

MOPKOBKA ★★★★★
() автор топика
Последнее исправление: MOPKOBKA (всего исправлений: 2)
Ответ на: комментарий от MOPKOBKA

Если верить википедии, то ML это 1984 год, так что вполне допотопный. Просто разное качество допотопности.

Нет. Это не так работает и это в принципе ещё одна проблема. То, что в википедии написано «сделано» это не значит сделано реально. А второе то что ты сейчас знаешь об «мл» и то, что было тогда - это две большие разницы.

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

Заметь что руками я написал только вот эти строки:

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

Пример с выражениями повторить невозможно из за отсутствия перегрузки

Я тебе специально обернул это в add/mul для примера. Есть/нет перегрузка неважно.

но про операцию над типами в теле я подумаю (хотя бы про реализацию с одним int_t), позже напишу если будут вопросы.

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

Свойство там одно - есть A и B и они преобразуются в C каким угодно образом. Тут наоборот пример многого не демонстрирует потому как тело у функций одинаковое.

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

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

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

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

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

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

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

Удивительно то насколько интересна ситуация. Различие настолько глобальное. Язык находится настолько далеко от того что могут осознать обыватель. Это реально как связывать космолёт с телегой. И объяснить это людям сложность. И даже не потому что они шизы(хотя адепты раста/всякой иного мусора из палеолита именно они), а потому что сложно даже осознать тот самый разрыв. Когда ты всю жизнь и везде и всюду видел телегу.

anonymous
()

С удовольствием прочитал страницы с врывом Царя. Я с ним не во всем согласен но спорить смысла не вижу, в любом случае он молодец.

Не сразу понял чем вторая категория отличается от первой - но таки да, в Crystal описан тип Proc в стдлибе, а в дельфи он черный ящик (хотя в обоих случаях понятно что он состоит из двух указателей).

kipar_2024
()
Ответ на: комментарий от anonymous

Нет. Это не так работает и это в принципе ещё одна проблема.

Потому и добавил «Если верить», если не верить, то для Standard ML есть документ, но это уже 1984 год. 80е это уже не совсем древность, но между Rust 1.0 и Standard ML разница 31 год.

Свойство там одно - есть A и B и они преобразуются в C каким угодно образом.

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

type 'a t = 
  | Array : 'a array -> 'a t
  | Bytes : bytes -> 'a t

(* Нельзя написать без указания типа вручную *)
let get (type el) (t:el t) i : el =
  match t with
  | Array a -> Array.get a i
  | Bytes s -> Bytes.get s i
Без указания того что функция get с аргументом el t возвращает el, никакой вывод не работает, и следовательно невозможно описать следующую функцию:
type 'a number_t =
  | Int : int -> int number_t
  | Float : float -> float number_t

let add (type tx ty) (x : tx number_t) (y : ty number_t) : 'c =
  match (x, y) with
  | (Int x, Int y) -> Int (x + y)
  | (Float x, Float y) -> Float (x +. y)
  | (Int x, Float y) | (Float y, Int x) -> Float ((float_of_int x) +. y)
Которая при сложении Int Int дает Int, Float Float дает Float, а вот для Int + Float дает повышение до Float. А в Haskell можно написать такую функцию? monk, hateyoufeel?

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

MOPKOBKA ★★★★★
() автор топика
Последнее исправление: MOPKOBKA (всего исправлений: 2)
Ответ на: комментарий от monk

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

MOPKOBKA ★★★★★
() автор топика
Последнее исправление: MOPKOBKA (всего исправлений: 1)
Ответ на: комментарий от monk

Мой пример вообще не работает, 'c не может быть разным для разных tx, ty. Описание типов я добавил для понятности того, чего я хочу добиться.

Ну и заметь, у меня тип входа конкретный нигде не указан как у тебя.

MOPKOBKA ★★★★★
() автор топика
Последнее исправление: MOPKOBKA (всего исправлений: 1)
Ответ на: комментарий от MOPKOBKA

Ну и заметь, у меня тип входа конкретный нигде не указан как у тебя.

Что значит «тип входа»? Если ты про шаблоны сопоставления после имени функции, то это просто синтаксис как match.

Могу написать

add a b = case a of
  (Int x) -> case b of
    (Int y) -> Int (x + y)
    (Float y) -> add b a
  (Float x) -> case b of
    (Int y) -> Float (x + fromIntegral y)
    (Float y) -> Float (x + y)  
monk ★★★★★
()
Ответ на: комментарий от monk

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

А Haskell имеет возможность в типы вставлять числа? Возможно получится повторить полный пример Царя. Мне достаточно понять, можно ли так:

template <int N> struct int_t {};

int_t<40> i40;
int_t<25> i25;

MOPKOBKA ★★★★★
() автор топика
Ответ на: комментарий от MOPKOBKA

А Haskell имеет возможность в типы вставлять числа? Возможно получится повторить полный пример Царя. Мне достаточно понять, можно ли так:

{-# LANGUAGE DataKinds #-}
import GHC.TypeLits

data IntT (n :: Natural) = IntT

a = IntT :: IntT 4096
monk ★★★★★
()
Ответ на: комментарий от MOPKOBKA

Твой пример выше реализует какую то перегрузку по варианту ADT как я понял?

То не перегрузка, то просто синтаксис match. Когда сопоставление по аргументам функции, в Haskell принято ветки сопоставления с повтором имени функции писать. Преобразуется всё равно в такой же case. Написать три строчки, потом что-то ещё, потом четвертую нельзя, как в Си++.

monk ★★★★★
()
Ответ на: комментарий от monk

А ещё можно сделать так, чтобы тип add был не Number -> Number -> Number, а один из Int -> Int -> Int, Float -> Int -> Float

{-# LANGUAGE TypeFamilies #-}

type family F a b where
  F Int Int  = Int
  F a Float = Float
  F Float a = Float
  F a b   = Float

class Number a b where
  add :: a -> b -> F a b

instance Number Int Int where add = (+)
instance Number Float Float where add = (+)
instance (Integral a) => Number Float a where add a b = add b a
instance (Integral a) => Number a Float where add a b = fromIntegral a + b
monk ★★★★★
()
Последнее исправление: monk (всего исправлений: 1)