Haskell 的 Agda 中的 Arrow-Class 和 Agda 中的 ->

Question

我有两个密切相关的问题:

首先，如何在 Agda 中建模/表示 Haskell 的 Arrow 类？

 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')

(下面的 Blog Post 表明它应该是可能的...)

其次，在 Haskell 中，(->) 是一等公民，也是另一种高阶类型，可以直接将 (->) 定义为Arrow 类的一个实例。但 Agda 的情况如何呢？我可能是错的，但我觉得 Agdas -> 比 Haskell 的 -> 是 Agda 更不可或缺的一部分。那么，Agdas -> 是否可以被视为高阶类型，即产生 Set 的类型函数，它可以成为 Arrow 的实例？

Answer 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)
  }