Давай я тебе объясню как работает их дерьмо. Там примитивная скриптуха. В ней нет того, что ты хочешь. Работает она по следующему принципу. В типы записывается всякое говно, далее путём всяких фокусов, хаков - формированию каких-то типов. Вот формирование этих типов с учётом всего кружаего говна - они называют доказательством. Как такого n + 1 - там нет.

Соответственно, на С++ нужно писать весь этот пердолинг. Особенно учитывая то, что в С++ типы полиморфны, а в скриптухе нет. Учитывая то, что в скриптухе одна убогая рекурсивная логика говна и никакой реальной.

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

Ничего. Я уже объяснял - С++ язык следующего порядка. Он не использует готовую арифметику - он её создаёт.

какой тип у NPE в Haskell?

Ну системы типов мы наблюдаем как не работают

NPE

и все такое

То завтипы в плюсах есть, то нет. Определиться бы

У меня есть вопрос к знающим людям. Всё никак понять не могу. Вот есть язык C++ и там нет завтипов, насколько я понял. И вот меня интересует следующие - почему. Т.е. чего системе типов С++ не хватает и что нужно добавить, чтобы каким-то образом реализовать/добавить завтипы?

Тогда какой смысл от кортежей если списки можно также использовать?

scala слишком усложнённый

Кто функциональное программирование умеет?

Желательно на python

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

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

и из-за того, что все конструкции имеют больше смысла - они и быстрее

[In reply to Roman na]
https://www.cl.cam.ac.uk/~jrh13/papers/cade05.html пойдет?

[In reply to Alex Gryzlov]
"Real Arithmetic" здесь - это совершенно не то. К тому же, "где-то кое как пытаются" и используется - это две не одно и тоже.

[In reply to Roman na]
это статья от исследователей Intel, их работы использовались для дизайна процессоров

[In reply to Alex Gryzlov]
Это громкие слова. Пруфов у нас нет. Тут это как работает. Есть деньги - можно исследовать. Не важно поможет/нет - хуже не сделает, но вдруг в чём-то поможет.