虽然 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)
}