Arrow-classe de Haskell en Agda et -> dans Agda

Question

J'ai deux questions étroitement liées:

Tout d'abord, comment la classe Arrow Haskell être modélisé/représenté dans 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') 

(le Blog Post suivant indique qu'il devrait être possible ...)

En second lieu, en Haskell, le (->) est un citoyen de première classe et juste un autre type d'ordre supérieur et son simple à définir (->) comme une instance de la classe Arrow. Mais comment ça se passe à Agda? Je peux me tromper, mais je pense, que Agdas -> est une partie plus intégrante d'Agda, que -> est de Haskell. Ainsi, Agdas -> peut-il être vu comme un type d'ordre supérieur, c'est-à-dire une fonction de type produisant Set qui peut être une instance de Arrow?

Answer 1

classes de type sont généralement codées sous forme d'enregistrements dans Agda, vous pouvez donc encoder la classe Arrow comme quelque chose comme ceci:

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

Alors que vous ne pouvez pas faire référence au type de fonction directement (quelque chose comme _→_ n'est pas syntaxe valide), vous pouvez écrire votre propre nom pour cela, que vous pouvez ensuite utiliser pour écrire une instance:

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

alors que la réponse de Hammar est un port correct du code Haskell, la définition de _=>_ est trop l imité par rapport à ->, car il ne supporte pas les fonctions dépendantes. En adaptant le code de Haskell, c'est un changement standard nécessaire si vous voulez appliquer vos abstractions aux fonctions que vous pouvez écrire dans Agda. En outre, par la convention habituelle de la bibliothèque standard, cette classe de type serait appelée RawArrow parce que pour l'implémenter, vous n'avez pas besoin de fournir des preuves que votre instance satisfait aux lois de la flèche; voir RawFunctor et RawMonad pour d'autres exemples (remarque: les définitions de Functor et Monad ne sont pas visibles dans la bibliothèque standard, à partir de la version 0.7).

Voici une variante plus puissante, que j'ai écrite et testée avec Agda 2.3.2 et la bibliothèque standard 0.7 (qui devrait aussi fonctionner sur la version 0.6). Notez que j'ai seulement changé la déclaration de type du paramètre RawArrow et de _=>_, le reste est inchangé. Cependant, lors de la création de fnArrow, toutes les autres déclarations de type ne fonctionnent pas comme auparavant.

Attention: J'ai seulement vérifié que le code typechecks et que => peut être utilisé raisonnablement, je n'ai pas vérifié si des exemples utilisant 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) 
    }