Чтобы немного попрактиковаться с 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