Haskell'a Arrow-Class w Agda oraz -> w Agda

Question

mam dwa ściśle powiązane pytania:

Po pierwsze, jak może Haskell'a Strzałka Klasa być modelowane/reprezentowane w 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') 

(następujące Blog Post stwierdza, że ​​powinno być możliwe ...)

Po drugie, w Haskell The (->) jest typ pierwszoklasowy i po prostu inny rodzaj wyższego rzędu, a jego proste do zdefiniowania (->) jako jedna instancja klasy Arrow. Ale jak to jest w Agdzie? Mogę się mylić, ale czuję, że Agdas -> jest bardziej integralną częścią Agdy, niż Haskella ->. Czy zatem Agdas -> może być postrzegany jako typ wyższego rzędu, tj. Funkcja typu, która daje Set, która może być wykonana jako instancja Arrow?

Answer 1

zajęcia typu są zazwyczaj kodowane jako rekordy w Agda, więc można zakodować klasę Arrow jak coś takiego:

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

Chociaż nie może odnosić się do rodzaju funkcji bezpośrednio (coś jak _→_ nie jest poprawna składnia), można napisać własną nazwę dla niej, które można następnie wykorzystać przy pisaniu instancję:

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

Chociaż odpowiedź Hammar jest poprawny port kodu Haskell, definicja _=>_ zbyt l naśladować w porównaniu do ->, ponieważ nie obsługuje funkcji zależnych. Kiedy dostosowujesz kod z Haskell, jest to standardowa konieczna zmiana, jeśli chcesz zastosować swoje abstrakcje do funkcji, które możesz napisać w Agdzie.

Co więcej, zgodnie z przyjętą konwencją standardowej biblioteki, ta typografia będzie miała nazwę RawArrow, ponieważ aby ją zaimplementować, nie trzeba udowadniać, że instancja spełnia prawa strzałki; zobacz RawFunctor i RawMonad dla innych przykładów (uwaga: definicje Functor i Monad są nigdzie w zasięgu wzroku w standardowej bibliotece, od wersji 0.7).

Oto mocniejszy wariant, który napisałem i przetestowałem z Agdą 2.3.2 i biblioteką standardową 0.7 (powinien również działać w wersji 0.6). Zauważ, że zmieniłem tylko deklarację typu parametru RawArrow i _=>_, reszta pozostała niezmieniona. Jednak przy tworzeniu fnArrow nie wszystkie deklaracje typów alternatywnych działają jak poprzednio.

Ostrzeżenie: Sprawdziłem tylko, czy kodowanie jest typowe i że można użyć>>, nie sprawdzałem, czy przykłady używają metody sprawdzania pisowni przy użyciu metody 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) 
    }