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

(以下博客文章指出它应该是可能的......)

其次,在Haskell中,它(->)是一流的公民,只是另一个更高阶的类型,它可以直接定义(->)为Arrow类的一个实例.但在阿格达怎么样？我可能是错的,但我觉得,Agdas ->是Agda的一个不可或缺的部分,而不是Haskell的->.那么,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)
  }