Perché i funtori Haskell hanno solo tipi derivati nella loro categoria di destinazione?

12

In Haskell, il functor typeclass Functor è definito come segue (vedi ad esempio Haskell wiki ):

class Functor (f :: * -> *) where
  fmap :: (a -> b) -> f a -> f b 

Per quanto comprendo (correggimi se ho torto), un tale functor può avere solo come categoria di destinazione una categoria costruita usando un costruttore di tipi, ad es. [] , Maybe , ecc. D'altro canto, si può pensare a funtori aventi qualsiasi categoria come obiettivo di un funtore, ad es. la categoria di tutti i tipi di Haskell. Ad esempio, Int potrebbe essere un oggetto nella categoria di destinazione di un funtore, non solo Maybe Int o [Int] .

Qual è la motivazione di questa restrizione sui funtori Haskell?

    
posta Giorgio 19.07.2014 - 22:24
fonte

1 risposta

2

Non ci sono restrizioni! Quando ho iniziato ad apprendere le basi teoriche di categoria per i costruttori di tipi, anche questo punto mi ha confuso. Ci arriveremo. Ma prima, lasciami chiarire un po 'di confusione. Queste due citazioni:

such a functor can only have as target category a category constructed using a type constructor

e

one may think of functors having any category as target of a functor, e.g. the category of all Haskell types

mostra che stai fraintendendo cosa sia un funtore (o per lo meno usi impropriamente la terminologia).

I Functional non costruiscono categorie. Un functor è una mappatura tra categorie. I Functional portano oggetti e morfismi (tipi e funzioni) nella categoria sorgente a oggetti e morfismi nella categoria target.

Si noti che ciò significa che un functor è in realtà una coppia di mappature: una mappatura sugli oggetti F_obj e una mappatura sui morfismi F_morph . In Haskell, la parte dell'oggetto F_obj del functor è il nome del costruttore del tipo (ad esempio List ), mentre la parte del morfismo è la funzione fmap (dipende dal compilatore Haskell per ordinare a quale fmap ci riferiamo in ogni espressione data). Quindi, non possiamo dire che List sia un functor; solo la combinazione di List e fmap è un funtore. Tuttavia, le persone abusano della notazione; i programmatori chiamano List un funtore, mentre i teorici delle categorie usano lo stesso simbolo per riferirsi a entrambe le parti del funtore.

Inoltre, nella programmazione, quasi tutti i funtori sono endofuntor , cioè la categoria di origine e di destinazione sono gli stessi - la categoria di tutti i tipi nella nostra lingua. Chiamiamo questa categoria Tipo . Un endofunctor F su Tipo mappa un tipo T a un altro tipo FT e una funzione T - & gt ; S a un'altra funzione FT - > FS . Questa mappatura deve ovviamente obbedire alle leggi del funtore.

Usando List come esempio: abbiamo un costruttore di tipi List : Type -> Type , e una funzione fmap: (a -> b) -> (List a -> List b) , che insieme formano un funtore. T

C'è un ultimo punto da chiarire. Scrivere List int non crea un nuovo tipo di elenchi di numeri interi. Questo tipo esisteva già . Era un oggetto nella nostra categoria Tipo . List Int è semplicemente un modo per fare riferimento ad esso.

Ora ti stai chiedendo perché un functor non può mappare un tipo per, ad esempio, Int o String . Ma può! Basta usare il functor di identità. Per ogni categoria C , il functor dell'identità mappa ogni oggetto su se stesso e il morfismo su se stesso. È semplice verificare che questa mappatura soddisfi le leggi del funtore. In Haskell, questo sarebbe un costruttore di tipi id : * -> * che esegue il mapping di ogni tipo su se stesso. Ad esempio, id int valuta int .

Inoltre, si possono persino creare funtori costanti , che mappano tutti i tipi in un singolo tipo. Ad esempio, il functor ToInt : * -> * , dove ToInt a = int per tutti i tipi a , e associa tutti i morfismi alla funzione di identità intera: fmap f = \x -> x

    
risposta data 05.10.2016 - 05:50
fonte

Leggi altre domande sui tag