Продолжаю ковырять. Вроде как всё, что я хотел бы от поддержки туплов, Агда умеет (туплы мои). По сути получается удобная работа с гетерогенным списком. Я, правда, не писал ещё всякие map/zip и прочие, но, надеюсь, там проблем не будет.
http://hpaste.org/68922
2) Нафига нужны туплы?
2. это же гетерогенный список
например, в моей библиотечке сериализации int .**. string .**. double будет иметь тип сериализатора для (Int, (String, Double)), который затем можно преобразовать в нужный тип данных, предоставив функцию из тупла и в тупл, генерящуюся на TH для нужного типа. Для поддержки нескольких конструкторов, разумеется, ещё Either используется.
Только вот int .**. (string .**. double) это вовсе не то же самое, что (int .**. string) .**. double
В зависимо типизированном языке роль tuple играет record. Всегда. Просто потому, что в произведении типов каждый аргумент имеет свой смысл.
Tuples, HList и Either это костыли, которые нужны в Х-е. В Agda они не нужны.
Напомню, у меня есть, грубо говоря, Serializer a, я могу несколько таких объединить и получить Serializer для тупла, который затем легко превращается в нужный рекорд.
Как мне обойтись без вспомогательного тупла?
Serializer при этом, не Applicative, он лишь Functor, и то для Iso a b = Iso (a -> b) (b -> a). Поэтому у меня есть только продукт и копродукт.
Идиоматично было бы генерировать биндинги c помощью какой-нибудь Template Agda, если бы она существовала. (Хотя, может, существует? Я слышал что-то про Reflection, но не копал.)
Без туплов действительно придётся либо пилить вручную для каждого рекорда, либо делать через туплы. :(
Идиоматичнее было бы, имхо, если бы для типа существовала функция (в случае для Test a = Some a | Some2 a [a], например):
test' :: Test a <-> Either a (a, [a])
а конструктор имел бы тип Some : a <?-> Test a, где a <?-> b = (a -> b, b -> Maybe a)
так как Test, всё же, это a + a * [a], просто с именами для каждого варианта.
Про Reflection я где-то у них видел упоминание, но пока не заглядывал.
Edited at 2012-05-25 09:40 am (UTC)