Почему (* 3) `map` (+100) не работает в Idris?

Question

В Haskell функции являются функторами, и следующий код работает как положено:

(*3) `fmap` (+100) $ 1

Выход 303, конечно. Однако в Idris (с fmap -> map) выдается следующая ошибка:

Не могу найти реализацию для Functor (\uv => Integer -> uv)

Мне кажется, что функции не реализованы как функторы в Idris, по крайней мере, не так, как в Haskell, но почему?

Кроме того, что именно означает сигнатура типа (\uv => Integer -> uv)? Это выглядит как некоторая частично примененная функция, и это то, что можно ожидать от реализации функтора, но синтаксис немного сбивает с толку, особенно то, что \, который предполагается использовать для лямбда / литерала, это делать там.

Answer 1

Функтор - это интерфейс. В Idris реализации ограничены данными или конструкторами типов, т.е. определены с помощью ключевого слова data. Я не эксперт в зависимых типах, но я считаю, что это ограничение требуется - практически, по крайней мере - для системы звукового интерфейса.

Когда вы спрашиваете тип \a => Integer -> a в REPL, вы получаете

\a => Integer -> a : Type -> Type

В Haskell мы считаем, что это настоящий конструктор типов, который можно превратить в экземпляр классов типов, таких как Functor. Однако в Idris (->) не является конструктором типов, а связывателем .

Самым близким к вашему примеру в Идрисе будет

((*3) `map` Mor (+100)) `applyMor` 1

с использованием модуля Data.morphisms . Или шаг за шагом:

import Data.Morphisms

f : Morphism Integer Integer
f = Mor (+100)

g : Morphism Integer Integer
g = (*3) `map` f

result : Integer
result = g `applyMor` 1

Это работает, потому что Morphism - это конструктор реального типа с реализацией Functor, определенной в библиотеке.