Профунктор Исо не печатает чек

Question

Пытаюсь реализовать простейшую профункторную оптику в Идрисе. Iso — это функция, которая должна быть полиморфной во всех профункторах. Я думаю, что это правильный синтаксис.

Все типовые проверки, кроме финального теста.

      interface Profunctor (p : Type -> Type -> Type) where
  dimap : (a' -> a) -> (b -> b') -> p a b -> p a' b'

Iso : Type -> Type -> Type -> Type -> Type
Iso a b s t = {p : Type -> Type -> Type} -> Profunctor p => p a b -> p s t

-- A pair of functions
data PairFun : Type -> Type -> Type -> Type -> Type where
  MkPair : (s -> a) -> (b -> t) -> PairFun a b s t

-- PairFun a b s t  is a Profunctor in s t
Profunctor (PairFun a b) where
  dimap f g (MkPair get set) = MkPair (get . f) (g . set)

-- Extract a pair of functions from an Iso
fromIso : Iso a b s t -> PairFun a b s t
fromIso iso = iso (MkPair id id)

-- Turn a pair of functions to an Iso
toIso : PairFun a b s t -> Iso a b s t
toIso (MkPair get set) = dimap get set

-- forall p. Profunctor p => p Int Int -> p Char String
myIso : Iso Int Int Char String
myIso = toIso (MkPair ord show)

x : PairFun Int Int Char String
x = fromIso myIso

Я получаю эту ошибку. Похоже, что Идрис жалуется на предположение, что p1 является профунктором, но это ограничение в определении Iso.

      Can't find implementation for Profunctor p1
    Type mismatch between
            p1 Int Int -> p1 Char String (Type of myIso p1
                                                         constraint)
    and
            p Int Int -> p Char String (Expected type)
                
     Specifically:
            Type mismatch between
                    p1 Int Int
            and
                    p Int Int

Answer 1

Следующий код работал у меня в Idris 2 версии 0.3. Это довольно старая версия Idris 2, но, вероятно, она работает и в более поздних версиях.

      interface Profunctor (0 p : Type -> Type -> Type) where
  dimap : (a' -> a) -> (b -> b') -> p a b -> p a' b'

Iso : Type -> Type -> Type -> Type -> Type
Iso a b s t = {0 p : Type -> Type -> Type} -> Profunctor p => p a b -> p s t

data PairFun : Type -> Type -> Type -> Type -> Type where
  MkPair : (s -> a) -> (b -> t) -> PairFun a b s t

Profunctor (PairFun a b) where
  dimap f g (MkPair get set) = MkPair (get . f) (g . set)

fromIso : Iso a b s t -> PairFun a b s t
fromIso iso = iso (MkPair id id)

toIso : PairFun a b s t -> Iso a b s t
toIso (MkPair get set) = dimap get set

myIso : Iso Int Int Char String
myIso = toIso (MkPair ord show)

x : PairFun Int Int Char String
x = fromIso myIso

К сожалению, я не знаю, как заставить это работать в Idris 1. Там проблема заключается в генеративности: разработчик не делает вывод из p1 a b = p2 a b. Ни в одном из Идрисов это вообще не выполняется, т.к. p1а также p2могут быть произвольными функциями. Идрис 2, кажется, переходит к p1 = p2в любом случае в какой-то момент; это удобная функция за счет некоторой надежности вывода.

Нерелевантные аннотации в приведенном выше коде не связаны с проблемой генеративности, о которой я только что упомянул, они просто необходимы для воспроизведения поведения Idris 1 и GHC. В Idris 2 неявно введенные переменные всегда имеют кратность, поэтому мы должны сделать так, чтобы pтакже стерты, чтобы можно было применить его к параметрам типа. Более того, 0 pсоответствует поведению Idris 1/GHC, где типы вообще стираются. В Idris 2 типы стираются только при привязке к 0.