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

Question

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

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

类的一个实例。但 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)
  }

Answer 2

虽然 hammar 的答案是 Haskell 代码的正确移植，但与

_=>_

相比，

->

的定义太有限，因为它不支持依赖函数。当改编 Haskell 的代码时，如果您想将抽象应用到可以在 Agda 中编写的函数，那么这是一个标准的必要更改。

此外，按照标准库的通常惯例，这个类型类将被称为

RawArrow

，因为要实现它，你不需要提供你的实例满足箭头定律的证明；请参阅 RawFunctor 和 RawMonad 了解其他示例（注意：从 0.7 版开始，Functor 和 Monad 的定义在标准库中看不到）。

这是一个更强大的变体，我使用 Agda 2.3.2 和 0.7 标准库编写并测试了它（也应该适用于 0.6 版本）。请注意，我只更改了

RawArrow

的参数和

_=>_

的类型声明，其余部分未更改。但是，在创建

fnArrow

时，并非所有替代类型声明都像以前一样工作。

警告：我只检查了代码类型检查以及 => 是否可以合理使用，我没有检查示例是否使用

RawArrow

类型检查。

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's more cumbersome:
test3 : Set
test3 = ℕ => (λ {n : ℕ} → Fin n)
--Note that since _=>_ uses Set instead of being level-polymorphic, it's 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)
  }