Bons exemplos de Not Functor / Functor / Applicative / Monad?

210

Enquanto explico para alguém o que é uma classe de tipo X, luto para encontrar bons exemplos de estruturas de dados que são exatamente X.

Então, peço exemplos para:

  • Um construtor de tipo que não é um Functor.
  • Um construtor de tipo que é um Functor, mas não Aplicável.
  • Um construtor de tipo que é um Candidato, mas não é uma Mônada.
  • Um construtor de tipo que é uma Mônada.

Eu acho que existem muitos exemplos de Mônada em todos os lugares, mas um bom exemplo de Mônada com alguma relação com exemplos anteriores poderia completar o quadro.

Eu procuro exemplos que sejam semelhantes entre si, diferindo apenas em aspectos importantes por pertencer à classe de tipo particular.

Se alguém conseguisse esgueirar-se para um exemplo de Arrow em algum lugar nessa hierarquia (é entre Applicativo e Mônada?), Isso seria ótimo também!

Rotsor
fonte
4
É possível criar um tipo constructor ( * -> *) para o qual não existe um adequado fmap?
Owen
1
Owen, acho que a -> Stringnão é um functor.
Rotsor 28/08/11
3
@Rotsor @Owen a -> Stringé um functor matemático, mas não um Haskell Functor, para ser claro.
J. Abrahamson
@J. Abrahamson, em que sentido é então um functor matemático? Você está falando da categoria com as setas invertidas?
Rotsor 04/04
3
Para as pessoas não sabem, um contravariant functor tem uma fmap do tipo(a -> b) -> f b -> f a
AJFarmar

Respostas:

100

Um construtor de tipo que não é um Functor:

newtype T a = T (a -> Int)

Você pode criar um functor contravariante, mas não um functor (covariante). Tente escrever fmape você irá falhar. Observe que a versão contravariante do functor é revertida:

fmap      :: Functor f       => (a -> b) -> f a -> f b
contramap :: Contravariant f => (a -> b) -> f b -> f a

Um construtor de tipo que é um functor, mas não é aplicável:

Eu não tenho um bom exemplo. Existe Const, mas, idealmente, eu gostaria de um não-monóide concreto e não consigo pensar em nenhum. Todos os tipos são basicamente numéricos, enumerações, produtos, somas ou funções quando você faz isso. Você pode ver abaixo pigworker e eu discordo sobre se Data.Voidé um Monoid;

instance Monoid Data.Void where
    mempty = undefined
    mappend _ _ = undefined
    mconcat _ = undefined

Como _|_é um valor legal em Haskell e, de fato, o único valor legal de Data.Void, isso atende às regras do Monoid. Não tenho certeza do que unsafeCoercetem a ver com isso, porque seu programa não tem mais garantia de não violar a semântica de Haskell assim que você usar qualquer unsafefunção.

Consulte o Wiki da Haskell para obter um artigo sobre as funções inferiores ( link ) ou inseguras ( link ).

Gostaria de saber se é possível criar esse tipo de construtor usando um sistema de tipo mais rico, como Agda ou Haskell com várias extensões.

Um construtor de tipo que é um Candidato, mas não uma Mônada:

newtype T a = T {multidimensional array of a}

Você pode criar um aplicativo com algo como:

mkarray [(+10), (+100), id] <*> mkarray [1, 2]
  == mkarray [[11, 101, 1], [12, 102, 2]]

Mas se você fizer uma mônada, poderá obter uma incompatibilidade de dimensão. Suspeito que exemplos como esse sejam raros na prática.

Um construtor de tipo que é uma Mônada:

[]

Sobre as setas:

Perguntar onde está uma flecha nessa hierarquia é como perguntar que tipo de forma "vermelho" é. Observe a incompatibilidade de tipos:

Functor :: * -> *
Applicative :: * -> *
Monad :: * -> *

mas,

Arrow :: * -> * -> *
Dietrich Epp
fonte
3
Boa lista! Eu sugeriria usar algo mais simples como Either aum exemplo para o último caso, pois é mais fácil de entender.
fuz 28/08
6
Se você ainda estiver procurando por um construtor de tipo que seja Aplicativo, mas não uma Mônada, um exemplo muito comum seria ZipList.
John L
23
_|_habita todos os tipos em *, mas o objetivo Voidé que você precise se curvar para construir um ou destrua seu valor. É por isso que não é uma instância de Enum, Monoid, etc. Se você já tem um, eu estou feliz que você mash-los juntos (dando-lhe um Semigroup), mas mempty, mas eu não dão ferramentas para construir explicitamente um valor do tipo Voidem void. Você precisa carregar a arma, apontá-la para o pé e puxar o gatilho.
Edward KMETT
2
Pedanticamente, acho que sua noção de Cofunctor está errada. O dual de um functor é um functor, porque você virar tanto a entrada e a saída e acabar com exatamente a mesma coisa. A noção que você está procurando é provavelmente "função contravariante", que é um pouco diferente.
Ben Millwood
1
@AlexVong: "Descontinuado" -> as pessoas estão apenas usando um pacote diferente. Falando sobre "functor contravariante", não "dual de functor", desculpe a confusão. Em alguns contextos, vi "cofunctor" usado para se referir a "functores contravariantes" porque os functores são autoduplos, mas parece ser apenas pessoas confusas.
Dietrich Epp
87

Meu estilo pode ser apertado pelo meu telefone, mas aqui vai.

newtype Not x = Kill {kill :: x -> Void}

não pode ser um Functor. Se fosse, teríamos

kill (fmap (const ()) (Kill id)) () :: Void

e a lua seria feita de queijo verde.

Entretanto

newtype Dead x = Oops {oops :: Void}

é um functor

instance Functor Dead where
  fmap f (Oops corpse) = Oops corpse

mas não pode ser aplicável, ou teríamos

oops (pure ()) :: Void

e Green seria feito com queijo Moon (o que pode realmente acontecer, mas apenas mais tarde à noite).

(Observação extra :, Voidcomo em Data.Voidé um tipo de dados vazio. Se você tentar undefinedprovar que é um Monoid, usarei unsafeCoercepara provar que não é.)

Com alegria,

newtype Boo x = Boo {boo :: Bool}

é aplicável de várias maneiras, por exemplo, como Dijkstra gostaria,

instance Applicative Boo where
  pure _ = Boo True
  Boo b1 <*> Boo b2 = Boo (b1 == b2)

mas não pode ser uma mônada. Para ver por que não, observe que o retorno deve ser constante Boo Trueou Boo False, e, portanto, que

join . return == id

não pode segurar.

Ah sim, eu quase esqueci

newtype Thud x = The {only :: ()}

é uma mônada. Role o seu próprio.

Avião para pegar ...

trabalhador de porcos
fonte
8
O vazio está vazio! Moralmente, de qualquer maneira.
pigworker
9
Void é um tipo com 0 construtores, presumo. Não é um monóide porque não existe mempty.
Rotsor 28/08
6
Indefinido? Que rude! Infelizmente, unsafeCoerce (unsafeCoerce () <*> indefinido) não é (); portanto, na vida real, existem observações que violam as leis.
pigworker
5
Na semântica usual, que tolera exatamente um tipo de indefinido, você está certo. Existem outras semânticas, é claro. Vazio não se restringe a um submonóide no fragmento total. Nem é um monóide em uma semântica que distingue modos de falha. Quando tiver um momento mais fácil do que a edição por telefone, vou esclarecer que meu exemplo funciona apenas em uma semântica para a qual não há exatamente um tipo indefinido.
pigworker
22
Muito barulho por_|_
Landei
71

Acredito que as outras respostas tenham perdido alguns exemplos simples e comuns:

Um construtor de tipo que é um Functor, mas não um Aplicativo. Um exemplo simples é um par:

instance Functor ((,) r) where
    fmap f (x,y) = (x, f y)

Mas não há como definir sua Applicativeinstância sem impor restrições adicionais r. Em particular, não há como definir pure :: a -> (r, a)para um arbitrário r.

Um construtor de tipo que é um Candidato, mas não é uma Mônada. Um exemplo conhecido é o ZipList . (É uma newtypelista que agrupa e fornece uma Applicativeinstância diferente para eles.)

fmapé definido da maneira usual. Mas puree <*>são definidos como

pure x                    = ZipList (repeat x)
ZipList fs <*> ZipList xs = ZipList (zipWith id fs xs)

assim purecria uma lista infinita, repetindo o valor dado, e <*>fecha uma lista de funções com uma lista de valores - aplica-se i função -ésimo para i -simo elemento. (O padrão <*>on []produz todas as combinações possíveis de aplicação da i- ésima função ao j- ésimo elemento.) Mas não há uma maneira sensata de definir uma mônada (veja este post ).


Como as setas se encaixam na hierarquia de functor / aplicativo / mônada? Veja Idiomas inconscientes, flechas são meticulosas, mônadas são promíscuas por Sam Lindley, Philip Wadler e Jeremy Yallop. MSFP 2008. (Eles chamam expressões de funções aplicadoras ).

Revisitamos a conexão entre três noções de computação: mônadas de Moggi, flechas de Hughes e expressões idiomáticas de McBride e Paterson (também chamadas de functores aplicativos). Mostramos que os idiomas são equivalentes às setas que satisfazem o isomorfismo do tipo A ~> B = 1 ~> (A -> B) e que as mônadas são equivalentes às setas que satisfazem o isomorfismo do tipo A ~> B = A -> (1 ~ B). Além disso, idiomas incorporados em flechas e flechas incorporadas em mônadas.

Petr Pudlák
fonte
1
O mesmo ((,) r)acontece com um functor que não é um aplicativo; mas isso ocorre apenas porque geralmente não é possível definir puretudo de ruma vez. É, portanto, uma peculiaridade da concisão de linguagem, de tentar definir uma coleção (infinita) de functores aplicativos com uma definição de puree <*>; nesse sentido, não parece haver nada matematicamente profundo sobre esse contra-exemplo, pois, para qualquer concreto r, ((,) r) pode ser transformado em um functor aplicativo. Pergunta: Você consegue pensar em um functor CONCRETE que deixa de ser um aplicativo?
George
1
Veja stackoverflow.com/questions/44125484/… como post com esta pergunta.
George
20

Um bom exemplo para um construtor de tipos que não é um functor é Set: Você não pode implementar fmap :: (a -> b) -> f a -> f b, porque sem uma restrição adicional, Ord bvocê não pode construir f b.

Landei
fonte
16
Na verdade, é um bom exemplo, pois matematicamente gostaríamos realmente de tornar isso um functor.
Alexandre C.
21
@AlexandreC. Eu discordo disso, não é um bom exemplo. Matematicamente, essa estrutura de dados forma um functor. O fato de não podermos implementar fmapé apenas uma questão de linguagem / implementação. Além disso, é possível envolver Seta mônada de continuação, que faz dela uma mônada com todas as propriedades que esperamos, veja esta pergunta (embora eu não tenha certeza se isso pode ser feito com eficiência).
Petr Pudlák 29/08/12
@PetrPudlak, como isso é um problema de idioma? A igualdade de bpode ser indecidível, nesse caso, você não pode definir fmap!
Turion
@Turion Ser decidível e definível são duas coisas diferentes. Por exemplo, é possível definir corretamente a igualdade nos termos lambda (programas), mesmo que não seja possível decidi-la por um algoritmo. De qualquer forma, este não foi o caso deste exemplo. Aqui, o problema é que não podemos definir uma Functorinstância com a Ordrestrição, mas isso pode ser possível com uma definição diferente Functorou com melhor suporte ao idioma. Na verdade, com o ConstraintKinds , é possível definir uma classe de tipo que pode ser parametrizada dessa maneira.
Petr Pudlák
Mesmo se pudéssemos superar a ordrestrição, o fato de que a Setnão pode conter entradas duplicadas significa que fmappoderia alterar o contexto. Isso viola a lei da associatividade.
John F. Miller
11

Eu gostaria de propor uma abordagem mais sistemática para responder a essa pergunta e também mostrar exemplos que não usam truques especiais, como os valores "inferiores" ou tipos de dados infinitos ou algo assim.

Quando os construtores de tipo falham em ter instâncias de classe de tipo?

Em geral, há duas razões pelas quais um construtor de tipos pode falhar ao ter uma instância de uma determinada classe de tipos:

  1. Não é possível implementar as assinaturas de tipo dos métodos necessários da classe de tipo.
  2. Pode implementar as assinaturas de tipo, mas não pode atender às leis exigidas.

Exemplos do primeiro tipo são mais fáceis do que aqueles do segundo tipo, porque, para o primeiro tipo, precisamos apenas verificar se é possível implementar uma função com uma determinada assinatura de tipo, enquanto que, para o segundo tipo, somos obrigados a provar que nenhuma implementação possivelmente poderia satisfazer as leis.

Exemplos específicos

  • Um construtor de tipo que não pode ter uma instância de functor porque o tipo não pode ser implementado:

    data F z a = F (a -> z)

Este é um contrafunctor, não um functor, com relação ao parâmetro type a, porque aem uma posição contravariante. É impossível implementar uma função com assinatura de tipo (a -> b) -> F z a -> F z b.

  • Um construtor de tipo que não é um functor legal, mesmo que a assinatura de tipo fmappossa ser implementada:

    data Q a = Q(a -> Int, a)
    fmap :: (a -> b) -> Q a -> Q b
    fmap f (Q(g, x)) = Q(\_ -> g x, f x)  -- this fails the functor laws!

O aspecto curioso deste exemplo é que nós podemos implementar fmapdo tipo correto, mesmo que Fnão pode ser um functor porque ele usa aem uma posição contravariant. Portanto, essa implementação fmapmostrada acima é enganosa - mesmo tendo a assinatura de tipo correta (acredito que essa seja a única implementação possível dessa assinatura de tipo), as leis do functor não são cumpridas. Por exemplo, fmap idid, porque let (Q(f,_)) = fmap id (Q(read,"123")) in f "456"é 123, mas let (Q(f,_)) = id (Q(read,"123")) in f "456"é 456.

De fato, Fé apenas um profunctor, - não é um functor nem um contrafunctor.

  • Um functor legal que não é aplicável porque a assinatura de tipo purenão pode ser implementada: pegue a mônada do Writer (a, w)e remova a restrição que wdeve ser um monóide. É então impossível construir um valor do tipo (a, w)fora de a.

  • Um functor que não é aplicativo porque a assinatura tipo de <*>impossibilidade de aplicação: data F a = Either (Int -> a) (String -> a).

  • Um functor que não é um aplicativo legal, mesmo que os métodos da classe de tipo possam ser implementados:

    data P a = P ((a -> Int) -> Maybe a)

O construtor de tipos Pé um functor porque ele usa aapenas em posições covariantes.

instance Functor P where
   fmap :: (a -> b) -> P a -> P b
   fmap fab (P pa) = P (\q -> fmap fab $ pa (q . fab))

A única implementação possível da assinatura de tipo <*>é uma função que sempre retorna Nothing:

 (<*>) :: P (a -> b) -> P a -> P b
 (P pfab) <*> (P pa) = \_ -> Nothing  -- fails the laws!

Mas essa implementação não satisfaz a lei de identidade para functores aplicativos.

  • Um functor que é, Applicativemas não um,Monad porque a assinatura do tipo bindnão pode ser implementada.

Eu não conheço nenhum desses exemplos!

  • Um functor que é, Applicativemas não é,Monad porque as leis não podem ser satisfeitas, mesmo que a assinatura do tipo bindpossa ser implementada.

Este exemplo gerou bastante discussão, portanto, é seguro dizer que provar que esse exemplo está correto não é fácil. Mas várias pessoas verificaram isso independentemente por métodos diferentes. Consulte Is `data PoE a = Empty | Emparelhar aa` uma mônada? para discussão adicional.

 data B a = Maybe (a, a)
   deriving Functor

 instance Applicative B where
   pure x = Just (x, x)
   b1 <*> b2 = case (b1, b2) of
     (Just (x1, y1), Just (x2, y2)) -> Just((x1, x2), (y1, y2))
     _ -> Nothing

É um tanto complicado provar que não existe um Monadcaso legal . A razão para o comportamento não-monádico é que não há uma maneira natural de implementar bindquando uma função f :: a -> B bpode retornar Nothingou Justpara valores diferentes de a.

Talvez seja mais claro considerar Maybe (a, a, a), que também não é uma mônada, e tentar implementar joinisso. Descobriremos que não há uma maneira intuitivamente razoável de implementar join.

 join :: Maybe (Maybe (a, a, a), Maybe (a, a, a), Maybe (a, a, a)) -> Maybe (a, a, a)
 join Nothing = Nothing
 join Just (Nothing, Just (x1,x2,x3), Just (y1,y2,y3)) = ???
 join Just (Just (x1,x2,x3), Nothing, Just (y1,y2,y3)) = ???
 -- etc.

Nos casos indicados por ???, parece claro que não podemos produzir de Just (z1, z2, z3)maneira razoável e simétrica dentre seis valores diferentes de tipo a. Certamente poderíamos escolher algum subconjunto arbitrário desses seis valores - por exemplo, sempre levar o primeiro não vazio Maybe- mas isso não satisfaria as leis da mônada. O retorno Nothingtambém não satisfará as leis.

  • Uma estrutura de dados em forma de árvore que não é uma mônada , embora tenha associação para bind- mas falha nas leis de identidade.

A mônada usual de árvore (ou "uma árvore com galhos em forma de functor") é definida como

 data Tr f a = Leaf a | Branch (f (Tr f a))

Esta é uma mônada livre sobre o functor f. A forma dos dados é uma árvore em que cada ponto de ramificação é um "functor-ful" de subárvores. A árvore binária padrão seria obtida com type f a = (a, a).

Se modificarmos essa estrutura de dados, fazendo também as folhas na forma do functor f, obteremos o que chamo de "semimonada" - ela bindsatisfaz as leis de naturalidade e associatividade, mas seu puremétodo falha em uma das leis de identidade. "Semimonados são semigrupos na categoria de endofuncionadores, qual é o problema?" Esta é a classe de tipo Bind.

Para simplificar, defino o joinmétodo em vez de bind:

 data Trs f a = Leaf (f a) | Branch (f (Trs f a))
 join :: Trs f (Trs f a) -> Trs f a
 join (Leaf ftrs) = Branch ftrs
 join (Branch ftrstrs) = Branch (fmap @f join ftrstrs)

O enxerto de ramo é padrão, mas o enxerto de folhas não é padrão e produz a Branch. Isso não é um problema para a lei de associatividade, mas quebra uma das leis de identidade.

Quando os tipos polinomiais têm instâncias de mônada?

Nenhum dos functores Maybe (a, a)e Maybe (a, a, a)pode receber uma Monadinstância legal , embora sejam obviamente Applicative.

Esses functores não têm truques - Voidnem bottomem nenhum lugar, nem em preguiça / rigidez complicada, nem em estruturas infinitas nem em restrições de classe de tipo. A Applicativeinstância é completamente padrão. As funções returne bindpodem ser implementadas para esses functores, mas não satisfazem as leis da mônada. Em outras palavras, esses functores não são mônadas porque falta uma estrutura específica (mas não é fácil entender exatamente o que está faltando). Como exemplo, uma pequena alteração no functor pode transformá-lo em uma mônada: data Maybe a = Nothing | Just aé uma mônada. Outro functor semelhante data P12 a = Either a (a, a)também é uma mônada.

Construções para mônadas polinomiais

Em geral, aqui estão algumas construções que produzem Monads legais a partir de tipos polinomiais. Em todas essas construções, Mhá uma mônada:

  1. type M a = Either c (w, a)onde westá algum monóide
  2. type M a = m (Either c (w, a))onde mestá qualquer mônada e wé qualquer monóide
  3. type M a = (m1 a, m2 a)onde m1e m2qualquer mônada
  4. type M a = Either a (m a)onde mtem mônada

A primeira construção é WriterT w (Either c), a segunda construção é WriterT w (EitherT c m). A terceira construção é um produto de mônadas em pure @Mtermos de componentes : é definido como o produto em termos de componentes de pure @m1e pure @m2, e join @Mé definido pela omissão de dados de produtos cruzados (por exemplo, m1 (m1 a, m2 a)é mapeado para m1 (m1 a)omissão da segunda parte da tupla):

 join :: (m1 (m1 a, m2 a), m2 (m1 a, m2 a)) -> (m1 a, m2 a)
 join (m1x, m2x) = (join @m1 (fmap fst m1x), join @m2 (fmap snd m2x))

A quarta construção é definida como

 data M m a = Either a (m a)
 instance Monad m => Monad M m where
    pure x = Left x
    join :: Either (M m a) (m (M m a)) -> M m a
    join (Left mma) = mma
    join (Right me) = Right $ join @m $ fmap @m squash me where
      squash :: M m a -> m a
      squash (Left x) = pure @m x
      squash (Right ma) = ma

Eu verifiquei que todas as quatro construções produzem mônadas legais.

I conjecturar que não existem outras construções para monads polinomiais. Por exemplo, o functor Maybe (Either (a, a) (a, a, a, a))não é obtido através de nenhuma dessas construções e, portanto, não é monádico. No entanto, Either (a, a) (a, a, a)é monádico, porque é isomorfo ao produto de três mônadas a, a, e Maybe a. Além disso, Either (a,a) (a,a,a,a)é monádico porque é isomórfico ao produto de ae Either a (a, a, a).

As quatro construções mostradas acima nos permitem obter qualquer soma de qualquer número de produtos de qualquer número de a's, por exemplo, Either (Either (a, a) (a, a, a, a)) (a, a, a, a, a))e assim por diante. Todos esses tipos de construtores terão (pelo menos uma) Monadinstância.

Resta saber, é claro, que casos de uso podem existir para essas mônadas. Outra questão é que as Monadinstâncias derivadas pelas construções 1-4 geralmente não são exclusivas. Por exemplo, o construtor de tipos type F a = Either a (a, a)pode receber uma Monadinstância de duas maneiras: pela construção 4 usando a mônada (a, a)e pela construção 3 usando o isomorfismo do tipo Either a (a, a) = (a, Maybe a). Novamente, encontrar casos de uso para essas implementações não é imediatamente óbvio.

Uma pergunta permanece - dado um tipo de dados polinomial arbitrário, como reconhecer se ele tem uma Monadinstância. Não sei como provar que não há outras construções para mônadas polinomiais. Não acho que exista nenhuma teoria até agora para responder a essa pergunta.

Winitzki
fonte
Eu acho que B é uma mônada. Você pode dar um contra-exemplo para esse vínculo Pair x y >>= f = case (f x, f y) of (Pair x' _,Pair _ y') -> Pair x' y' ; _ -> Empty?
Franky
A Associatividade @Franky falha com essa definição quando você escolhe ftal que f xé Emptymas f yé um Paire, no próximo passo, ambos são Pair. Eu verifiquei manualmente que as leis não se aplicam a esta implementação ou a qualquer outra implementação. Mas é um bom trabalho fazer isso. Eu gostaria que houvesse uma maneira mais fácil de descobrir isso!
winitzki
1
@ Turion Esse argumento não se aplica, Maybeporque Maybenão contém valores diferentes apara se preocupar.
Daniel Wagner
1
@Turion Eu provei isso em algumas páginas de cálculos; o argumento sobre "caminho natural" é apenas uma explicação heurística. Uma Monadinstância consiste em funções returne bindque satisfazem leis. Existem duas implementações returne 25 implementações bindque se encaixam nos tipos necessários. Você pode mostrar, por cálculo direto, que nenhuma das implementações atende às leis. Para reduzir a quantidade de trabalho necessária, eu usei joinem vez de binde usaram as leis de identidade pela primeira vez. Mas tem sido um bom trabalho.
winitzki
1
@duplode Não, acho que não Traversableé necessário. m (Either a (m a))é transformado usando pure @mem m (Either (m a) (m a)). Então trivialmente Either (m a) (m a) -> m a, e podemos usar join @m. Essa foi a implementação para a qual eu verifiquei as leis.
winitzki