но можно

не, там другая система. Там просто уточнения типов. У тебя есть vec<n> где n такой же затёртый тип. Внутри функция так же не полиморфна, но ты можешь уточнить тип

это как если бы в расте было <T>(x: T) if(x == int) { x ==int }

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

так же там pm вынесен на уровень сигнатур

но так не советуют делать, кк я уже говорил

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

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

а он относительно C++

Ну сложно сказать. Ну, допустим, из такого самого очевидного. Если мы делим условный nat на 1 или 2, то мы этого сделать не можем. В ситуации же когда мы знаем, что нам приходит - мы можем учесть только то, что нам нужно. Там уже будет не nat, а 1 или 2

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

Т.е. за идеал я рассматриваю именно подобную комбинацию.

увы я немного не догнал что имеется в виду

смотри, вот у тебя есть f(Nat)

у неё область определения - все числа

натуральные. в С++ ты можешь задать Nat, но смысл в том, что область определения будут "все используемые числа"

если ты будешь f вызывать только для f(1); f(2); - там будут только 1 и 2, а не все возможные натуральные числа. И тебе хватит матча по 1 или 2, что ты не сможешь сделать в ситуации с nat и тебе нужно будет добавить _ и какой-то костыль для выхода

отвечу на тему sum. Рядовой полиморфизм настолько сильно въелся в мозг людей, что они пишут его как T add<T>(x: T, y: T), потому как они думают, что операции такие же мономорфные и  числа мономорфные. Эта мономорфность везде. И если мы предположим, что наши типы - это числа, то мы получаем: во-первых ошибку add(1, 2). Во-вторых результатом у нас будет являться 1 или 2, т.е. add в прнципе не выразим через подобную сигнатуру

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

ну тут вопрос о том, что первично а что вторично.

В моем мире контракт функции первичен - она определяет, что она умеет работать с 1, 2 но не с 3. И функции которые её вызывают должны это учитывать, а она соответственно может матчить только 2 возможных варианта.

А если получается наоборот, мы дергаем функцию с разными аргументами, а потом внутри функции знаем, что нас вызывали с 3,5,7 и 12 и мы должны их как-то обработать, получается что caller - главный, а callee под него подстравивается. Кмк это неудобно, потому что во-первых размазывает зону ответственности функции, её скоуп теперь не только сигнатуры + тело, но ещё и все возможные способы обработки. Во-вторых не представляю как это должно работать при например динамическом связаывании, когда наша функция лежит в dll и мы никак не можем знать кто с какими аргументами её использует

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

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


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