haskell - applicative functor

¿Hay un Functor que no pueda ser aplicable a la ley?

Question

Una pregunta reciente hecha en general sobre los límites entre varias clases de Haskell. Se me ocurrió Handler como ejemplo de un Functor válido sin una instancia sensible de Apply **, donde

class Functor f => Apply f where
  (<.>) :: f (a -> b) -> f a -> f b
  -- optional bits omitted.

Sin embargo, aún no he podido encontrar un ejemplo de un Functor válido que no pueda convertirse en una instancia válida (si no tiene sentido) de Apply . El hecho de que Apply haya tenido (ver actualización) pero una sola ley,

(.) <$> u <.> v <.> w = u <.> (v <.> w)

Parece que esto es bastante complicado.

pigworker (Conor McBride) previamente dio un ejemplo de un Functor que no es Applicative , pero se basó en pure para hacerlo, y eso no está disponible en Apply .

** Luego, más tarde, me di cuenta de que en realidad podría haber una instancia de Apply sensible (aunque algo extraña) para Handler , que recopila conceptualmente excepciones simultáneas.

Actualizar

Edward Kmett ahora ha accepted dos leyes adicionales que propuse para Apply (para validar las optimizaciones que hice en la instancia de Apply (Coyoneda f) ):

x <.> (f <$> y) = (. f) <$> x <.> y
f <$> (x <.> y) = (f .) <$> x <.> y

Sería interesante ver si estas adiciones cambian la respuesta a esta pregunta.

Answer 1

Esto no es exactamente lo que estás buscando, pero está cerca, así que pensé en compartirlo. La mónada estándar de Writer tiene una restricción adicional en su instancia de Apply (es decir, que el tipo w es una instancia de Semigroup o Semigroup ) que la instancia de Functor no tiene, por lo que Writer Foo es un Functor pero no se Apply si Foo no es un Semigroup / Monoid :

data Writer w a = Writer w a

instance Monoid w => Apply (Writer w) where
  Writer w1 f <.> Writer w2 x = Writer (mappend w1 w2) (f x)

Sin embargo, este no es realmente un ejemplo de lo que estás pidiendo, porque en realidad es posible crear una instancia de Apply Monoid ley sin una restricción Monoid :

instance Apply (Writer w) where
  Writer w1 f <.> Writer w2 x = Writer w1 (f x)

El problema con esta instancia es que no permite una instancia Applicative coincidente, ya que no habría manera de implementar pure tal manera que obtenga una identidad izquierda, es decir:

pure id <.> x /= x

Esta es solo una manera larga de darte la misma respuesta que ya tenías de Conor: una demostración que se basa en pure para romper la instancia.

Answer 2

La "suma" de dos functors ( Data.Functor.Sum from transformers ) parece ser un ejemplo.

Uno puede mapear fácilmente sobre una rama u otra, pero ¿cómo implementar <.> Cuando la función en el funtor y el argumento en el funtor se encuentran en diferentes ramas?

ghci> import Data.Functor.Sum
ghci> import Data.Functor.Identity
ghci> let f = InL (Const ())   :: Sum (Const ()) Identity (Int -> Int)
ghci> let x = InR (Identity 5) :: Sum (Const ()) Identity Int
ghci$ f <.> x = ..... ?

Answer 3

Sí, hay Functor s sin instancia de Apply . Considere la suma de dos funciones (que son exponentes en los tipos de datos algebraicos ):

data EitherExp i j a
    = ToTheI (i -> a)
    | ToTheJ (j -> a)

Hay una instancia de Functor para todos los i s y j s:

instance Functor (EitherExp i j) where
    fmap f (ToTheI g) = ToTheI (f . g)
    fmap f (ToTheJ g) = ToTheJ (f . g)

pero no hay una instancia de Apply para todos i s y j s

instance Apply (EitherExp i j) where
    ...
    ToTheI f <.> ToTheJ x = ____

No hay manera de llenar el espacio en blanco ____ . Para hacerlo, tendríamos que saber algo acerca de i y j , pero no hay manera de mirar dentro de cada tipo i o j en Haskell. La intuición rechaza esta respuesta; Si sabe algo acerca de i o j , al igual que están habitados por un solo valor, puede escribir una instancia de Apply para EitherExp

class Inhabited a where
    something :: a

instance (Inhabited i, Inhabited j) => Apply (EitherExp i j) where
    ...
    ToTheI f <.> ToTheJ x = ToTheI (const ((f something) (x something)))

Pero no sabemos que cada i y cada j están Inhabited . El tipo Void no está habitado por nada. Ni siquiera tenemos una manera de saber que cada tipo es Inhabited o Void .

Nuestra intuición es realmente muy buena; cuando podemos inspeccionar cómo se construyen los tipos, para los tipos de datos algebraicos no hay ningún Functor que no tenga instancias de Apply . Lo que sigue son dos respuestas que pueden ser más agradables a nuestra intuición.

No ...

... para tipos de datos algebraicos. Hay 3 posibilidades. La estructura es nula, la estructura puede estar vacía o la estructura no puede estar vacía. Si la estructura es nula, entonces es una Apply absurd . Si puede estar vacío, elija cualquier instancia vacía y devuélvala constantemente para cualquier solicitud. Si no puede estar vacío, entonces es una suma de estructuras que cada una no puede estar vacía, se puede hacer una aplicación respetuosa de la ley aplicando uno de los valores ^† del primero a uno de los valores del segundo y devolviéndolo En alguna estructura constante.

La ley aplicable es muy laxa. Aplicar no tiene por qué tener ningún sentido. No necesita ser "zip-y". No necesita ser fmap cuando se combina con cosas sospechosas como pure de Applicative ; no hay noción de pure con la cual escribir una ley que requiera que tenga sentido.

Cuando la estructura puede estar vacía

Elija cualquier instancia vacía y devuélvala constantemente para cualquier solicitud

u <.> v = empty

Prueba

  (.) <$> u  <.> v  <.> w = u <.> (v <.> w)
(((.) <$> u) <.> v) <.> w = u <.> (v <.> w) -- by infixl4 <$>, infixl4 <.>
(_                ) <.> w = u <.> (_      ) -- by substitution
                    empty = empty           -- by definition of <.>

Cuando la estructura no puede estar vacía.

Si la estructura f no puede estar vacía, existe una función extract :: forall a. fa -> a extract :: forall a. fa -> a . Elija otra función c :: forall a. a -> fa c :: forall a. a -> fa que siempre construye la misma estructura no vacía rellena con el argumento en todas partes y define:

u <.> v = c (extract u $ extract v)

Con los teoremas libres.

extract (f <$> u) = f (extract u)
extract . c = id

Prueba

  (.) <$> u  <.> v  <.> w = u <.> (v <.> w)
(((.) <$> u) <.> v) <.> w = u <.> (v <.> w) -- by infixl4 <$>, infixl4 <.>
(c (extract ((.) <$> u) $ extract v)) <.> w = u <.> (v <.> w) -- by definition
(c ((.) (extract u)     $ extract v)) <.> w = u <.> (v <.> w) -- by free theorem 
c (extract (c ((.) (extract u) $ extract v)) $ extract w) = u <.> (v <.> w) -- by definition
c (           ((.) (extract u) $ extract v)  $ extract w) = u <.> (v <.> w) -- by extract . c = id
c (((.) (extract u) $ extract v) $ extract w) = u <.> c (extract v $ extract w) -- by definition
c (((.) (extract u) $ extract v) $ extract w) = c (extract u $ extract (c (extract v $ extract w))) -- by definition
c (((.) (extract u) $ extract v) $ extract w) = c (extract u $            (extract v $ extract w) ) -- by extract . c = id
let u'' = extract u
    v'' = extract v
    w'' = extract w
c (((.) u'' $ v'') $ w'') = c (u'' $ (v'' $ w''))
c ((u'' . v'') $ w'') = c (u'' $ (v'' $ w'')) -- by definition of partial application of operators
c (u'' $ (v'' $ w'')) = c (u'' $ (v'' $ w'')) -- by definition of (.)

Un poco más merece ser dicho acerca de la definición de extract para los tipos exponenciales, funciones. Para una función i -> a hay dos posibilidades. O estoy habitado o no lo está. Si está habitada, elija algún habitante i ^† y defina

extract f = f i

Si i está deshabitado (es nulo), entonces i -> a es el tipo de unidad con el único valor absurd . Void -> a es simplemente otro tipo de vacío que no contiene ninguna a s; Trátela como una estructura que puede estar vacía.

Cuando la estructura es nula.

Cuando la estructura es nula no hay formas de construirla. Podemos escribir una función única de cada construcción posible (no hay ninguna para pasarla) a cualquier otro tipo.

absurd :: Void -> a
absurd x = case x of {}

Las estructuras fmap f = absurd pueden ser fmap f = absurd con fmap f = absurd . De la misma manera pueden tener una instancia de Apply con

(<.>) = absurd

Podemos probar trivialmente que para todos u , v y w

(.) <$> u  <.> v  <.> w = u <.> (v <.> w)

No hay u , v o w y la afirmación es vacuamente verdadera .

^† Con algunas advertencias sobre la aceptación del axioma de elección para elegir un índice a para el tipo exponencial a -> b

Si ...

... por Haskell. Imagina que hay otra base de Monad diferente a IO , llamémosla OI . Entonces Sum IO OI es un Functor pero nunca puede ser un Apply .

... para el mundo real. Si tiene una máquina a la que puede enviar funciones (o flechas en una categoría que no sea Hask ), pero no puede combinar dos de las máquinas ni extraer su estado de ejecución, entonces son un Functor sin Aplicación.