Haskells Pfeil-Klasse in Agda und -> in Agda

Question

habe ich zwei eng verwandte Fragen:

Erstens: Wie kann die Haskells Pfeil Klasse in Agda modelliert/dargestellt werden?

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

(die folgenden Blog Post besagt, dass es möglich sein sollte ...)

Zweitens in Haskell, die (->) ist ein Bürger erste Klasse und nur eine weitere höhere Ordnung Art und seine einfach zu definieren (->) als eine Instanz der Arrow Klasse. Aber wie ist das in Agda? Ich könnte mich irren, aber ich fühle, dass Agdas -> ist ein integraler Bestandteil von Agda, als Haskell -> ist. Kann also Agdas -> als ein Typ höherer Ordnung angesehen werden, d. H. Eine Typfunktion, die Set ergibt, die zu einer Instanz von Arrow gemacht werden kann?

Answer 1

Typ-Klassen sind in der Regel als Datensätze in Agda codieren, so dass Sie die Arrow Klasse als so etwas wie dieses kodieren:

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

Während Sie nicht direkt auf den Funktionstyp beziehen (etwas _→_ wie nicht gültige Syntax), können Sie einen eigenen Namen für sie schreiben, die Sie dann verwenden, wenn eine Instanz zu schreiben:

_=>_ : 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

Während hammar Antwort eine korrekte Port des Haskell-Code ist, ist die Definition von _=>_ zu l imitiert im Vergleich zu ->, da es keine abhängigen Funktionen unterstützt. Wenn Sie Code von Haskell anpassen, ist das eine notwendige Änderung, wenn Sie Ihre Abstraktionen auf die Funktionen anwenden wollen, die Sie in Agda schreiben können.

Darüber hinaus würde diese Typenklasse nach der üblichen Konvention der Standardbibliothek RawArrow genannt werden, weil Sie für die Implementierung keine Beweise dafür benötigen, dass Ihre Instanz die Pfeilgesetze erfüllt; Weitere Beispiele finden Sie unter RawFunctor und RawMonad (Hinweis: Definitionen von Functor und Monad sind in der Standardbibliothek ab Version 0.7 nicht mehr verfügbar).

Hier ist eine leistungsfähigere Variante, die ich geschrieben und getestet habe mit Agda 2.3.2 und der 0.7 Standardbibliothek (sollte auch auf Version 0.6 funktionieren). Beachten Sie, dass ich nur die Typ-Deklaration von RawArrow Parameter und _=>_ geändert habe, der Rest ist unverändert. Bei der Erstellung von fnArrow funktionieren jedoch nicht alle alternativen Typdeklarationen wie zuvor.

Warnung: Ich habe nur überprüft, dass der Code typechecks und das => vernünftig verwendet werden kann, ich habe nicht überprüft, ob Beispiele mit RawArrow typecheck.

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