Agda2 tuples

[voidex]

Продолжаю ковырять. Вроде как всё, что я хотел бы от поддержки туплов, Агда умеет (туплы мои). По сути получается удобная работа с гетерогенным списком. Я, правда, не писал ещё всякие map/zip и прочие, но, надеюсь, там проблем не будет.
http://hpaste.org/68922

Comments

[udpn]

1) Нафига там duo?
2) Нафига нужны туплы?

[voidex]

1. duo там как просто тип данных, хоть какой-нибудь
2. это же гетерогенный список
например, в моей библиотечке сериализации int .**. string .**. double будет иметь тип сериализатора для (Int, (String, Double)), который затем можно преобразовать в нужный тип данных, предоставив функцию из тупла и в тупл, генерящуюся на TH для нужного типа. Для поддержки нескольких конструкторов, разумеется, ещё Either используется.

Только вот int .**. (string .**. double) это вовсе не то же самое, что (int .**. string) .**. double

[udpn]

Да, я в курсе, что правильно реализованные tuple это гетерогенные списки. Только вопрос снова тот же самый: нафига?

В зависимо типизированном языке роль tuple играет record. Всегда. Просто потому, что в произведении типов каждый аргумент имеет свой смысл.

Tuples, HList и Either это костыли, которые нужны в Х-е. В Agda они не нужны.

[voidex]

Ну так я же описал, зачем это нужно мне. Может, в зависимо типизированном языке есть какой-то common-way, тогда подскажите.

Напомню, у меня есть, грубо говоря, Serializer a, я могу несколько таких объединить и получить Serializer для тупла, который затем легко превращается в нужный рекорд.
Как мне обойтись без вспомогательного тупла?

Serializer при этом, не Applicative, он лишь Functor, и то для Iso a b = Iso (a -> b) (b -> a). Поэтому у меня есть только продукт и копродукт.