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

\elim это считай case-of

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

Do ghc follows tail call elimination? And does this make haskell faster and executes functions in constant memory space?

Yes, it does! And yes, such functions are evaluating faster and using a constant space.

Smart & interesting from systems point of view

TCO has disadvantages too, for instance, you lose stack trace (if you had)

по-моему в sicp было утверждение, что "цикл это просто синтаксический сахар над рекурсией". В случае TCO это даже правда.

"синтаксическая соль"

Как раз читаю этот момент...

Если бы не было TCO, то практические программы вообще невозможно было бы писать, разве нет? Потому что бесконечный цикл не написать для машины с конечной памятью.

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

можно писать практические программы без бесконечных циколов!

в кложе вот нету ТСО, но там рекурсия это сахар над циклом 8)

О, давно искал группу, где можно поговорить о языках, транслирующихся в код низкоуровневой машины без TCO

Так вот, про python...

Привет, подскажите пожалуйста. Хочу создать тип с динамическими полями, как это сделать? Например, у меня будет список названий полей, например ['id', 'firstname', 'lastname'],  я из него хочу динамически получить тип User:

data User = User
    { id :: Id User
    , firstname :: Text
    , lastname :: Text
    }

Соответсвенно, если список будет другой, например [id, firstname, lastname, email, password], то и тип должен быть с соответствующими полями. В питоне сделать такое проще простого, а тут как?

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

Есть ещё более сложные штуки вроде extensible records. Но тут уже нужно экспериментировать и смотреть какая из реализаций вам больше подойдёт.

В конце концов всегда можно взять Value из aeson и кодировать наборы полей как object. Проще говоря, если ваши данные представимы в виде JSON, то и в виде Value они будут представимы.

Вот только вы не можете получить новый тип на лету. По крайней мере — обычный record.

Можно лишь "перейти на сторону динамической типизации" (использование Map или Value и будет своеобразной ДТ).