Почему в Idris параметры интерфейса должны быть типом или конструктором данных?
Чтобы немного попрактиковаться с Idris, я пытался представить различные базовые алгебраические структуры в качестве интерфейсов. Сначала я решил организовать вещи так, чтобы параметры заданного интерфейса были заданы, а различные операции над ним, а методы / поля были доказательством различных аксиом. Например, я думал об определении Group вот так:
Group (G : Type) (op : G -> G -> G) (e : G) (inv : G -> G) where
assoc : {x,y,z : G} -> (x `op` y) `op z = x `op` (y `op` z)
id_l : {x : G} -> x `op` e = x
id_r : {x : G} -> x `op` e = x
inv_l : {x : G} -> x `op` (inv x) = e
inv_r : {x : G} -> (inv x) `op` x = e
Мои доводы сделать это таким образом, вместо того, чтобы просто сделать op, e, а также inv методы были в том, что было бы легче говорить о том, что один и тот же набор является группой по-разному. Мол, математически не имеет смысла говорить о том, что набор - это группа; имеет смысл говорить только о множестве, в котором указанная операция является группой. Один и тот же набор может соответствовать двум совершенно разным группам, определяя операцию по-разному. С другой стороны, доказательства различных законов интерфейса не влияют на группу. Хотя жители (доказательства) законов могут отличаться, это не приводит к другой группе. Таким образом, было бы бесполезно объявлять несколько реализаций.
Более фундаментально, этот подход кажется лучшим представлением математических понятий. Говорить о том, что набор является группой, - это ошибка категории, поэтому математик во мне не в восторге от того, что утверждает групповую операцию как интерфейсный метод.
Однако эта схема невозможна. Когда я пытаюсь, он на самом деле выполняет проверку типов, но как только я пытаюсь определить экземпляр, это не так: idris жалуется, что, например:
(+) cannot be a parameter of Algebra.Group
(Implementation arguments must be type or data constructors)
Мой вопрос: почему это ограничение? Я полагаю, что есть веская причина, но я не вижу ее в жизни. Например, я думал, что Idris сворачивает иерархию "значение / тип / вид", поэтому между типами и значениями нет реальной разницы, так почему же реализации обрабатывают типы специально? И почему конструкторы данных обрабатываются специально? Это кажется мне произвольным.
Теперь я мог бы добиться того же, используя именованные реализации, что, я думаю, я в итоге и сделаю сейчас. Я думаю, я просто привык к Haskell, где вы можете иметь только один экземпляр класса типов для данного типа данных. Но это все еще кажется довольно произвольным... В частности, я хотел бы иметь возможность определить, например, полукольцо как кортеж (R,+,*,0,1) где (R,+,0) это моноид и (R,*,1) является моноидом (с привязанными законами дитрибутивности). Но я не думаю, что смогу сделать это очень легко без вышеуказанной схемы, даже с именованными реализациями. Я мог бы только сказать, является ли R моноидом - но для полуколец он должен быть моноидом двумя различными способами! Я уверен, что есть обходные пути с некоторыми синонимами типового образца или чем-то еще (что, опять же, я, вероятно, в конечном итоге сделаю), но я не понимаю, почему это необходимо.
$ idris --version
1.2.0