13

密接に関連する2つの質問があります。

まず、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では、(->)は一級市民であり、もう1つの高階型であり、クラス(->)の1つのインスタンスとして定義するのは簡単です。Arrowしかし、それはAgdaではどうですか？私は間違っているかもしれませんが、Agdas->はHaskellのものよりもAgdaのより不可欠な部分であると感じてい->ます。したがって、Agdas->は高次の型、つまり、 ？Setのインスタンスにすることができる型関数を生成するものと見なすことができますArrowか？

4

2 に答える 2

15

型クラスは通常、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)
  }
于 2012-10-28T20:41:32.543 に答える
5

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)
  }
于 2013-01-30T21:41:43.540 に答える