Подтвердить что ты не робот

Выполнение количественной оценки ранжирования в Идрисе

Я могу делать только ранг-n типов в Idris 0.9.12 довольно неуклюжим способом:

tupleId : ((a : Type) -> a -> a) -> (a, b) -> (a, b)
tupleId f (a, b) = (f _ a, f _ b)

Мне нужны символы подчеркивания везде, где есть приложение типа, потому что Idris бросает ошибки разбора, когда я пытаюсь сделать неявные (вложенные) аргументы типа:

tupleId : ({a : Type} -> a -> a) -> (a, b) -> (a, b) -- doesn't compile

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

appShow :: Show a => (forall a. Show a => a -> String) -> a -> String
appShow show x = show x

Это также мешает мне использовать функции Idris как синонимы типов для таких типов, как Lens, который Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t в Haskell.

Любой способ исправить или обойти вышеупомянутые проблемы?

4b9b3361

ОТВЕТЫ

Ответ 1

Я только что реализовал это в master, позволяя имплицировать в произвольных областях, и это будет в следующем выпуске хака. Тем не менее, это еще не проверено! Я, по крайней мере, попробовал следующие простые примеры и несколько других:

appShow : Show a => ({b : _} -> Show b => b -> String) -> a -> String
appShow s x = s x

AppendType : Type
AppendType = {a, n, m : _} -> Vect n a -> Vect m a -> Vect (n + m) a

append : AppendType
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

tupleId : ({a : _} -> a -> a) -> (a, b) -> (a, b)
tupleId f (a, b) = (f a, f b)

Proxy  : Type -> Type -> Type -> Type -> (Type -> Type) -> Type -> Type

Producer' : Type -> (Type -> Type) -> Type -> Type
Producer' a m t = {x', x : _} -> Proxy x' x () a m t

yield : Monad m => a -> Producer' a m ()

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