di Haskell Arrow-Class in Agda e -> in Agda

Question

Ho due domande strettamente correlati:

In primo luogo, come può il Haskell classe Freccia essere modellato/rappresentato in 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') 

(il seguente Blog Post afferma che dovrebbe essere possibile ...)

In secondo luogo, in Haskell, il (->) è un cittadino di prima classe e solo un altro tipo di ordine superiore e la sua semplice da definire (->) come un'istanza della classe Arrow. Ma come è fatto ad Agda? Potrei sbagliarmi, ma ritengo che Agdas -> sia una parte più integrante di Agda, rispetto a quella di Haskell ->. Quindi, Agdas -> può essere visto come un tipo di ordine superiore, vale a dire una funzione di tipo che produce Set che può essere resa un'istanza di Arrow?

Answer 1

classi-tipo sono solitamente codificati come record in Agda, in modo da poter codificare la classe Arrow come qualcosa di simile a questo:

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

Anche se non si può fare riferimento al tipo di funzione direttamente (qualcosa come _→_ non è valida sintassi), è possibile scrivere il proprio nome per esso, che è possibile utilizzare quando si scrive un esempio:

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

Mentre la risposta di Hammar è una porta corretta del codice Haskell, la definizione di _=>_ è troppo l imitato rispetto a ->, poiché non supporta le funzioni dipendenti. Quando si adatta il codice da Haskell, si tratta di una modifica standard necessaria se si desidera applicare le astrazioni alle funzioni che è possibile scrivere in Agda.

Inoltre, dalla solita convenzione della libreria standard, questo typeclass sarebbe chiamato RawArrow perché per la sua attuazione non è necessario fornire prove che l'istanza soddisfa le leggi freccia; vedere RawFunctor e RawMonad per altri esempi (nota: le definizioni di Functor e Monad non sono presenti nella libreria standard, a partire dalla versione 0.7).

Ecco una variante più potente, che ho scritto e testato con Agda 2.3.2 e la libreria standard 0.7 (dovrebbe funzionare anche con la versione 0.6). Si noti che ho modificato solo la dichiarazione di tipo del parametro RawArrow e di _=>_, il resto è invariato. Tuttavia, quando si crea fnArrow, non tutte le dichiarazioni di tipo alternative funzionano come prima.

Avvertenza: ho controllato che il codice digitato e quello => possano essere utilizzati in modo ragionevole, non ho verificato se esempi utilizzano il typececk 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) 
    }