haskell - Agda中Haskell类的箭头和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, (->)是一等公民,只是另一个高阶类型及其简单的定义 (->)作为的一个实例 Arrowclass 。 但这怎么在Agda? 也可能我是错的,但我觉得,Agdas ->是一个比Haskells更Agda的整数部分, ->是什么。 大家能Agdas ->被视为是某种高级类型,我如果不包含。 从而产生一个类型函数 Set它可以使实例 Arrow?

时间: 原作者:

type类通常编码为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)
  }
原作者:

hammar时Haskell的答案是对端口的定义代码, _=>_太窄相比, ->,因为它不支持相关功能。 从Haskell改写代码时,这是一个标准的必要更改Agda中如果要应用加以抽象,你可以编写函数。

此外,对在标准库的常规约定,这个typeclass也将受到 RawArrow因为要实现它,无需提供校样,满足你的实例键的其他示例,请参见RawFunctor和RawMonad法令( note: Functor的定义以及Monad哪儿也没有其他地方在标准库,自版本0 0.7 ) 。

这是一个更强大的变量,这些我编写和测试带Agda 2 .3 .2和0 .7标准库( 版本0 。6 上也应该可用) 。 请注意,我只更改了类型声明。 RawArrow是的参数, _=>_,其余的保持不变。 在创建 fnArrow不过,并非所有其他工作与前面的类型声明。

warNING : 我只和这代码typechecks检查=>可合理地使用,我没有检查是否使用示例 RawArrowtypecheck 。

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)
  }
原作者:
...