Haskell Arrow-Class в Агда и → в Агда

У меня есть два тесно связанных вопроса:

Во-первых, как класс Haskell Arrow может быть смоделирован/представлен в Agda?

 class Arrow a where 
      arr :: (b -> c) -> a b c
      (>>>) :: a b c -> a c d -> a b d
      first :: a b c -> a (b,d) (c,d)
      second :: a b c -> a (d,b) (d,c)
      (***) :: a b c -> a b' c' -> a (b,b') (c,c')
      (&&&) :: a b c -> a b c' -> a b (c,c')

(следующая Сообщение в блоге гласит, что это должно быть возможно...)

Во-вторых, в Haskell (->) является первоклассным гражданином и просто еще одним типом более высокого порядка, и его просто определить (->) как один экземпляр класса Arrow. Но как это происходит в Агда? Я мог ошибаться, но я чувствую, что Agdas -> является более неотъемлемой частью Agda, чем Haskell ->. Таким образом, Agdas -> можно рассматривать как тип более высокого порядка, т.е. Функцию типа, дающую Set, которая может быть сделана экземпляром Arrow?

Ответ 1

Типовые классы обычно кодируются как записи в Agda, поэтому вы можете кодировать класс Arrow как-то вроде этого:

open import Data.Product -- for tuples

record Arrow (A : Set → Set → Set) : Set₁ where
  field  
    arr    : ∀ {B C} → (B → C) → A B C
    _>>>_  : ∀ {B C D} → A B C → A C D → A B D
    first  : ∀ {B C D} → A B C → A (B × D) (C × D)
    second : ∀ {B C D} → A B C → A (D × B) (D × C)
    _***_  : ∀ {B C B' C'} → A B C → A B' C' → A (B × B') (C × C')
    _&&&_  : ∀ {B C C'} → A B C → A B C' → A B (C × C')

Пока вы не можете напрямую ссылаться на тип функции (что-то вроде _→_ не является допустимым синтаксисом), вы можете написать свое собственное имя для него, которое вы можете использовать при записи экземпляра:

_=>_ : Set → Set → Set
A => B = A → B

fnArrow : Arrow _=>_  -- Alternatively: Arrow (λ A B → (A → B)) or even Arrow _
fnArrow = record
  { arr    = λ f → f
  ; _>>>_  = λ g f x → f (g x)
  ; first  = λ { f (x , y) → (f x , y) }
  ; second = λ { f (x , y) → (x , f y) }
  ; _***_  = λ { f g (x , y) → (f x , g y) }
  ; _&&&_  = λ f g x → (f x , g x)
  }

Ответ 2

В то время как ответ hammar является правильным портом кода Haskell, определение _=>_ слишком ограничено по сравнению с ->, поскольку оно не поддерживает зависимые функции. При адаптации кода из Haskell это стандартное необходимое изменение, если вы хотите применить свои абстракции к функциям, которые вы можете написать в Agda.

Кроме того, по обычному стандарту стандартной библиотеки этот класс будет называться RawArrow, потому что для его реализации вам не нужно предоставлять доказательства того, что ваш экземпляр удовлетворяет законам стрелок; см. RawFunctor и RawMonad для других примеров (примечание: определения Functor и Monad нигде не видны в стандартной библиотеке, начиная с версии 0.7).

Здесь более мощный вариант, который я написал и протестировал с помощью Agda 2.3.2 и стандартной библиотеки 0.7 (также должен работать на версии 0.6). Обратите внимание, что я только изменил объявление типа параметра RawArrow и _=>_, остальное не изменилось. При создании fnArrow, однако, не все объявления альтернативного типа работают по-прежнему.

Предупреждение: я только проверял, что код typechecks и that = > можно использовать разумно, я не проверял, используют ли примеры RawArrow typecheck.

module RawArrow where

open import Data.Product --actually needed by RawArrow
open import Data.Fin     --only for examples
open import Data.Nat     --ditto

record RawArrow (A : (S : Set) → (T : {s : S} → Set) → Set) : Set₁ where
  field  
    arr    : ∀ {B C} → (B → C) → A B C
    _>>>_  : ∀ {B C D} → A B C → A C D → A B D
    first  : ∀ {B C D} → A B C → A (B × D) (C × D)
    second : ∀ {B C D} → A B C → A (D × B) (D × C)
    _***_  : ∀ {B C B' C'} → A B C → A B' C' → A (B × B') (C × C')
    _&&&_  : ∀ {B C C'} → A B C → A B C' → A B (C × C')

_=>_ : (S : Set) → (T : {s : S} → Set) → Set
A => B = (a : A) -> B {a}

test1 : Set
test1 = ℕ => ℕ
-- With → we can also write:
test2 : Set
test2 = (n : ℕ) → Fin n
-- But also with =>, though it more cumbersome:
test3 : Set
test3 = ℕ => (λ {n : ℕ} → Fin n)
--Note that since _=>_ uses Set instead of being level-polymorphic, it still
--somewhat limited. But I won't go the full way.

--fnRawArrow : RawArrow _=>_
-- Alternatively:
fnRawArrow : RawArrow (λ A B → (a : A) → B {a})

fnRawArrow = record
  { arr    = λ f → f
  ; _>>>_  = λ g f x → f (g x)
  ; first  = λ { f (x , y) → (f x , y) }
  ; second = λ { f (x , y) → (x , f y) }
  ; _***_  = λ { f g (x , y) → (f x , g y) }
  ; _&&&_  = λ f g x → (f x , g x)
  }