Por que os functores Haskell só têm tipos derivados em sua categoria de destino?

12

No Haskell, o functor da classe de tipos Functor é definido da seguinte forma (consulte, por exemplo, wiki do Haskell ):

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

Tanto quanto eu entendo (por favor me corrijam se eu estiver errado), tal functor só pode ter como alvo categoria uma categoria construída usando um construtor de tipo, por exemplo [], Maybe, etc. Por outro lado, pode-se pensar em functors com qualquer categoria como alvo de um functor, por exemplo, a categoria de todos os tipos de Haskell. Por exemplo, Intpoderia ser um objeto na categoria de destino de um functor, não apenas Maybe Intou [Int].

Qual é a motivação para essa restrição nos funcionadores Haskell?

Giorgio
fonte
4
Simplicidade? Haskell não possui funções de tipo de primeira classe, portanto, todas as funções são realmente apenas construtores de tipo.
precisa
2
@jozefg: Perdoe minha ignorância: o que são "funções do tipo primeira classe"?
Giorgio
4
Então, nessa função, estamos jogando à fdireita? E no seu cenário, fdeve ser como uma função Haskell normal e mapear tipos para tipos. Em Haskell, as únicas coisas que podem ter esse tipo * -> *são construtores de tipo. Famílias tipográficas são mais gerais, mas devem sempre ser totalmente aplicado
Daniel Gratzer
@jozefg: Ocasionalmente penso nessa questão repetidamente. Suponho que a restrição de Haskell não afeta o poder expressivo dos functores. Por exemplo, suponha que tenhamos um functor isomórfico para o functor da lista, mas que não mapeie, digamos, Int -> [Int] mas Int -> <tipo sofisticado usando nenhum construtor de tipo>. Então eu acho que alguém poderia provar que <fantasia do tipo sem construtor de tipo> é isomórfica para [Int]. Portanto, escolher objetos que são definidos usando um construtor de tipos é apenas conveniente e não sacrifica o poder expressivo.
Giorgio

Respostas:

1

Não há nenhuma restrição! Quando comecei a aprender a base teórica da categoria para construtores de tipos, esse mesmo ponto também me confundiu. Nós vamos chegar a isso. Mas primeiro, deixe-me esclarecer alguma confusão. Estas duas citações:

esse functor pode ter apenas como categoria de destino uma categoria construída usando um construtor de tipo

e

pode-se pensar em functores tendo qualquer categoria como alvo de um functor, por exemplo, a categoria de todos os tipos de Haskell

mostre que você está entendendo mal o que é um functor (ou pelo menos está usando mal a terminologia).

Functors não constroem categorias. Um functor é um mapeamento entre categorias. Os fundores trazem objetos e morfismos (tipos e funções) na categoria de origem para objetos e morfismos na categoria de destino.

Observe que isso significa que um functor é realmente um par de mapeamentos: um mapeamento nos objetos F_obj e um mapeamento nos morfismos F_morph . Em Haskell, a parte do objeto F_obj do functor é o nome do construtor de tipos (por exemplo List), enquanto a parte do morfismo é a função fmap(cabe ao compilador Haskell classificar a que fmapestamos nos referindo em qualquer expressão). Assim, não podemos dizer que Listé um functor; apenas a combinação de Liste fmapé um functor. Ainda assim, as pessoas abusam da notação; os programadores chamam Listum functor, enquanto os teóricos da categoria usam o mesmo símbolo para se referir às duas partes do functor.

Além disso, na programação, quase todos os functores são endofuncionadores , ou seja, a categoria de origem e destino são os mesmos - a categoria de todos os tipos em nossa linguagem. Vamos chamar essa categoria de Tipo . Um endofuncor F no tipo mapeia um tipo T para outro tipo FT e uma função T -> S para outra função FT -> FS . É claro que esse mapeamento deve obedecer às leis do functor.

Usando Listcomo exemplo: temos um construtor de tipos List : Type -> Typee uma função fmap: (a -> b) -> (List a -> List b)que juntos formam um functor. T

Há um último ponto a esclarecer. A escrita List intnão cria um novo tipo de lista de números inteiros. Este tipo já existia . Foi um objeto em nossa categoria Tipo . List Inté simplesmente uma maneira de se referir a ele.

Agora, você está se perguntando por que um functor não pode mapear um tipo para, digamos, Intou String. Mas pode! Basta usar o functor de identidade. Para qualquer categoria C , o functor de identidade mapeia todos os objetos para si e o morfismo para si. É fácil verificar se esse mapeamento satisfaz as leis do functor. Em Haskell, esse seria um construtor de tipos id : * -> *que mapeia todos os tipos para si. Por exemplo, id intavalia como int.

Além disso, pode-se até criar functores constantes , que mapeiam todos os tipos para um único tipo. Por exemplo, o functor ToInt : * -> *, onde ToInt a = intpara todos os tipos a, e mapeia todos os morfismos para a função de identidade inteira: fmap f = \x -> x

Gardenhead
fonte
Obrigado pela sua resposta, esta pergunta tem mais de dois anos. "Functors não constroem categorias.": Eu não disse isso. Eu disse que os functores mapeiam duas categorias, onde a categoria de destino deve ter a forma f a, onde fé, até onde eu sei, um construtor de tipos. Pelo que me lembro da teoria das categorias, deve ser algum tipo de representação canônica (objeto inicial em uma categoria de categorias? Talvez esteja usando mal a terminologia.) De qualquer forma, vou ler sua resposta com atenção. Muito Obrigado.
Giorgio
@Giorgio grita, eu não percebi quantos anos tinha haha. Apenas apareceu em "perguntas não respondidas". Não sei ao certo o que você quer dizer com "representação canônica". Tanto quanto eu sei (e posso estar errado aqui), não existe uma relação entre functores e objetos iniciais / terminais.
precisa saber é o seguinte
Quero dizer isto: en.wikipedia.org/wiki/Initial_algebra (consulte Uso em ciência da computação). Em Haskell (a maioria), os functores são definidos em tipos de dados algébricos. O objeto alvo desse functor é uma álgebra inicial. A álgebra inicial é isomórfica ao conjunto de termos construídos usando os construtores de valor. Por exemplo, para listas []e :. Eu quis dizer isso por representação canônica.
Giorgio
Sim, eu sei o que é um objeto inicial e que tipos de dados indutivos são objetos iniciais na álgebra F de uma categoria. Você está certo de que muitos construtores de tipos são definidos indutivamente. Mas isso não é estritamente necessário. Por exemplo, o functor (_, int)que leva um tipo apara o tipo de produto (a, int)e uma função f : 'a -> 'bpara g : 'a * int -> 'a * intnão é indutivo.
precisa saber é o seguinte
Você quis dizer: "leva ... uma função f : 'a -> 'bpara g : 'a * int -> 'b * int?"
Giorgio