Есть ли хороший способ использовать `->` непосредственно как функцию в Idris?

Можно вернуть тип в функцию в Idris, например

t : Type -> Type -> Type
t a b = a -> b

Но возникла ситуация (при экспериментировании с написанием некоторых парсеров), что я хотел использовать -> для сворачивания списка типов, то есть

typeFold : List Type -> Type
typeFold = foldr1 (->)

Чтобы typeFold [String, Int] дал String -> Int : Type. Это не скомпилировано:

error: no implicit arguments allowed
    here, expected: ")",
    dependent type signature,
    expression, name
typeFold = foldr1 (->)
                   ^

Но это прекрасно работает:

t : Type -> Type -> Type
t a b = a -> b

typeFold : List Type -> Type
typeFold = foldr1 t

Есть ли лучший способ работы с ->, и если нет, то стоит ли его поднимать как запрос функции?

Ответ 1

Проблема с использованием -> таким образом заключается в том, что это не конструктор типа, а связующее, где имя, привязанное к домену, находится в области видимости в диапазоне, поэтому -> сам не имеет типа непосредственно, Например, ваше определение t не будет захватывать зависимый тип, например (x : Nat) -> P x.

Хотя это немного нерешительно, то, что вы делаете, это правильный способ сделать это. Я не уверен, что мы должны сделать специальный синтаксис для (->) как конструктор типа - отчасти потому, что он действительно не один, а отчасти потому, что похоже, что это приведет к большей путанице, когда оно не будет работать с зависимыми типами.

Ответ 2

Модуль Data.Morphisms предоставляет что-то вроде этого, за исключением того, что вы должны сделать все обертывание/разворот вокруг Morphism "newtype".