?

Log in

No account? Create an account
Previous Entry Share Next Entry
Agda2 tuples
eye
voidex
Продолжаю ковырять. Вроде как всё, что я хотел бы от поддержки туплов, Агда умеет (туплы мои). По сути получается удобная работа с гетерогенным списком. Я, правда, не писал ещё всякие map/zip и прочие, но, надеюсь, там проблем не будет.
http://hpaste.org/68922
Tags: ,

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

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

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


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

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

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

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

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

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

Что-то я в прошлый раз совсем не понял use case.

Идиоматично было бы генерировать биндинги 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)

  • 1