Зачем мне функтор Identity в Идрисе

Question

Несмотря на то, что Idris типизирован зависимо, где значения могут свободно использоваться в типах, он по-прежнему различает функцию id и функтор Identity. Почему я не могу определить экземпляры Functor для id:

Functor id where
  map = id

Тип id равен id : a -> a, поэтому a нельзя объединить с Type, так что map @{Functor id} имеет тип (a -> b) -> id a -> id b, который просто (a -> b) -> a -> b

Я понимаю, что Identity - это оболочка типа, но зачем мне нужен отдельный идентификатор на уровне типа, просто чтобы включить реализацию экземпляров класса типов.

Единственное отличие Identity и id состоит в том, что Identity a не может быть оценено как a, но это все еще функция Type -> Type, аналогичная id {a=Type} по типу.

Answer 1

id - это функция, которая возвращает свое входное значение в качестве результата. Если вам нужна функция, которая ничего не делает со своим входом, кроме как возвращает то же значение, тогда используйте id.

Identity - это оболочка простого типа, которая упаковывает тип t для создания нового типа Identity t, где значение типа Identity t - это запись, содержащая только одно значение исходного упакованного типа t .

Поскольку Identity является алгебраическим типом данных, он может реализовать интерфейс в Idris. В частности, он реализует Monad.

Иногда можно определить конструктор типов, который создает типы, которые реализуют Monad, сначала определив монадный преобразователь, который принимает монадический тип в качестве одного из своих параметров. Чтобы обеспечить произвольный немонадный тип в качестве параметра для такого конструктора, сначала оберните немонадный тип, используя конструктор типа Identity.

Например, см. Библиотечный модуль Control.Monad.Writer.