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

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

首先，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')

(以下 Blog Post 说明它应该是可能的......)

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

最佳答案

类型类通常在 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)
  }

关于Haskell 在 Agda 中的 Arrow-Class 和 -> 在 Agda，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/13112642/