haskell - tipograficas - ¿Puedo restringir una familia de tipos?

tipos de letras

Question

En esta reciente respuesta mía , casualmente abrí este viejo castaño (un programa tan antiguo, la mitad de él fue escrito en el siglo diecisiete por Leibniz y escrito en una computadora en los años setenta por mi padre). Dejaré fuera el bit moderno para ahorrar espacio.

class Differentiable f where
type D f :: * -> *
newtype K a x = K a
newtype I x = I x
data (f :+: g) x = L (f x)
| R (g x)
data (f :*: g) x = f x :&: g x
instance Differentiable (K a) where
type D (K a) = K Void
instance Differentiable I where
type D I = K ()
instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where
type D (f :+: g) = D f :+: D g
instance (Differentiable f, Differentiable g) => Differentiable (f :*: g) where
type D (f :*: g) = (D f :*: g) :+: (f :*: D g)

Ahora, aquí está lo frustrante. No sé cómo estipular que D f debe ser en sí mismo diferenciable. Ciertamente, estas instancias respetan esa propiedad, y podría haber programas divertidos que puedas escribir y que hagan uso de la capacidad de seguir diferenciando un functor, disparando agujeros en más y más lugares: expansiones de Taylor, ese tipo de cosas.

Me gustaría poder decir algo como

class Differentiable f where
type D f
instance Differentiable (D f)

y requieren un control de que las declaraciones de instancia tienen definiciones de type para las cuales existen las instancias necesarias.

Tal vez cosas más mundanas como

class SortContainer c where
type WhatsIn c
instance Ord (WhatsIn c)
...

también sería bueno Eso, por supuesto, tiene la solución fundep

class Ord w => SortContainer c w | c -> w where ...

pero intentar el mismo truco para Differentiable parece ... bueno ... involucionado.

Entonces, ¿hay alguna solución ingeniosa que me permita una diferenciabilidad repetible? (Creo que podría construir una representación GADT yy ... pero ¿hay alguna manera de que funcione con las clases?)

¿Y hay algún inconveniente obvio con la sugerencia de que deberíamos poder exigir restricciones en las familias de tipo (y, supongo, de datos) cuando las declaramos, y luego verificar que las instancias las satisfagan?

Answer 1

Ciertamente, lo más obvio sería simplemente escribir la restricción deseada directamente:

class (Differentiable (D f)) => Differentiable (f :: * -> *) where

Por desgracia, GHC se pone malhumorado y se niega a seguir el juego:

ConstrainTF.hs:17:1:
Cycle in class declaration (via superclasses):
Differentiable -> Differentiable
In the class declaration for `Differentiable''

Entonces, como suele ser el caso cuando intentamos describir las restricciones de tipo lo suficientemente imaginativas como para dejar a GHC recalcitrante, debemos recurrir a algún tipo de engaño.

Recordando algunas características relevantes de GHC donde está involucrado el tipo de hackeo:

• Es paranoico sobre la no determinación del nivel de tipo muy desproporcionada a las molestias reales que conlleva para el usuario.
• Se comprometerá alegremente a tomar decisiones sobre clases e instancias antes de considerar toda la información disponible.
• Obedientemente intentará verificar todo lo que haya engañado para comprometerse.

Estos son los principios tortuosos que subyacen a las viejas instancias faux-genéricas familiares, donde los tipos se unifican post-hoc con (~) para mejorar el comportamiento de inferencia de tipo de ciertos tipos de construcciones de hackeo.

En este caso, sin embargo, en lugar de pasar furtivamente la información del tipo más allá de GHC, tendríamos que evitar de alguna manera que GHC note una restricción de clase , que es un tipo completamente diferente de ... heeeey, waaaitaminute ....

import GHC.Prim
type family DiffConstraint (f :: * -> *) :: Constraint
type instance DiffConstraint f = Differentiable f
class (DiffConstraint (D f)) => Differentiable (f :: * -> *) where
type D f :: * -> *

¡Alce por su propio petardo!

Es el verdadero negocio, también. Estos son aceptados, como esperarías:

instance Differentiable (K a) where
type D (K a) = K Void
instance Differentiable I where
type D I = K ()

Pero si le ofrecemos algunas tonterías en su lugar:

instance Differentiable I where
type D I = []

GHC nos presenta precisamente el mensaje de error que nos gustaría ver:

ConstrainTF.hs:29:10:
No instance for (Differentiable [])
arising from the superclasses of an instance declaration
Possible fix: add an instance declaration for (Differentiable [])
In the instance declaration for `Differentiable I''

Hay un pequeño inconveniente, por supuesto, que es esto:

instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where
type D (f :+: g) = D f :+: D g

... resulta menos que bien fundado, ya que le hemos dicho a GHC que verifique que, siempre que (f :+: g) sea Differentiable , también lo es (D f :+: D g) , que no termina bien (o en absoluto).

La forma más fácil de evitar esto sería, por lo general, repetir un montón de casos base explícitos, pero aquí GHC parece tener la intención de divergir cada vez que aparece una restricción Differentiable en un contexto de instancia. Asumiría que está innecesariamente ansioso por controlar las limitaciones de la instancia de alguna manera, y tal vez podría distraerse lo suficiente con otra capa de engaños, pero no estoy seguro de por dónde empezar inmediatamente y he agotado mi capacidad para el hackeo de esta noche después de la medianoche.

Un poco de discusión IRC sobre #haskell logró trotar ligeramente mi memoria sobre cómo GHC maneja las restricciones de contexto de clase, y parece que podemos arreglar un poco las cosas con una familia de restricciones más exigente. Usando esto:

type family DiffConstraint (f :: * -> *) :: Constraint
type instance DiffConstraint (K a) = Differentiable (K a)
type instance DiffConstraint I = Differentiable I
type instance DiffConstraint (f :+: g) = (Differentiable f, Differentiable g)

Ahora tenemos una recursión mucho más correcta para las sumas:

instance (Differentiable (D f), Differentiable (D g)) => Differentiable (f :+: g) where
type D (f :+: g) = D f :+: D g

Sin embargo, el caso recursivo no se puede dividir fácilmente para productos, y la aplicación de los mismos cambios mejoró solo en la medida en que recibí un desbordamiento de pila de reducción de contexto en lugar de simplemente colgar en un bucle infinito.

Answer 2

Con las nuevas UndecidableSuperclasses en GHC 8

class Differentiable (D f) => Differentiable (f :: Type -> Type) where

trabajos.

Answer 3

Esto se puede lograr de la misma manera que sugiere Edward con una pequeña implementación de Dict . Primero, eliminemos las extensiones e importaciones de idiomas.

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
import Data.Proxy

TypeOperators es solo para su problema de ejemplo.

Tiny Dict

Podemos hacer nuestra propia implementación pequeña de Dict . Dict usa un GADT y ConstraintKinds para capturar cualquier restricción en el constructor para un GADT.

data Dict c where
Dict :: c => Dict c

withDict y withDict2 introducir la restricción mediante la coincidencia de patrones en GADT. Solo necesitamos poder razonar sobre los términos con una o dos fuentes de restricciones.

withDict :: Dict c -> (c => x) -> x
withDict Dict x = x
withDict2 :: Dict a -> Dict b -> ((a, b) => x) -> x
withDict2 Dict Dict x = x

Tipos infinitamente diferenciables

Ahora podemos hablar de tipos infinitamente diferenciables, cuyas derivadas también deben ser diferenciables

class Differentiable f where
type D f :: * -> *
d2 :: p f -> Dict (Differentiable (D f))
-- This is just something to recover from the dictionary
make :: a -> f a

d2 toma un proxy para el tipo y recupera el diccionario para tomar la segunda derivada. El proxy nos permite especificar fácilmente de qué tipo de d2 estamos hablando. Podemos llegar a diccionarios más profundos aplicando d :

d :: Dict (Differentiable t) -> Dict (Differentiable (D t))
d d1 = withDict d1 (d2 (pt (d1)))
where
pt :: Dict (Differentiable t) -> Proxy t
pt = const Proxy

Capturando el dictonario

Los tipos de funcionador polinomial, productos, sumas, constantes y cero son infinitamente diferenciables. Definiremos los testigos d2 para cada uno de estos tipos

data K x = K deriving (Show)
newtype I x = I x deriving (Show)
data (f :+: g) x = L (f x)
| R (g x)
deriving (Show)
data (f :*: g) x = f x :&: g x deriving (Show)

El cero y las constantes no requieren ningún conocimiento adicional para capturar el Dict sus derivados

instance Differentiable K where
type D K = K
make = const K
d2 = const Dict
instance Differentiable I where
type D I = K
make = I
d2 = const Dict

Tanto la suma como el producto requieren que los diccionarios de los derivados de ambos componentes puedan deducir el diccionario para su derivada.

instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where
type D (f :+: g) = D f :+: D g
make = R . make
d2 p = withDict2 df dg $ Dict
where
df = d2 . pf $ p
dg = d2 . pg $ p
pf :: p (f :+: g) -> Proxy f
pf = const Proxy
pg :: p (f :+: g) -> Proxy g
pg = const Proxy
instance (Differentiable f, Differentiable g) => Differentiable (f :*: g) where
type D (f :*: g) = (D f :*: g) :+: (f :*: D g)
make x = make x :&: make x
d2 p = withDict2 df dg $ Dict
where
df = d2 . pf $ p
dg = d2 . pg $ p
pf :: p (f :*: g) -> Proxy f
pf = const Proxy
pg :: p (f :*: g) -> Proxy g
pg = const Proxy

Recuperando el diccionario

Podemos recuperar el diccionario de restricciones que de otra manera no tendríamos la información adecuada para deducir. Differentiable f normalmente solo permitiría que el uso llegue a make :: a -> fa , pero no para make :: a -> D fa o make :: a -> D (D f) a .

make1 :: Differentiable f => p f -> a -> D f a
make1 p = withDict (d2 p) make
make2 :: Differentiable f => p f -> a -> D (D f) a
make2 p = withDict (d (d2 p)) make

Answer 4

Su mejor opción podría ser definir algo utilizando el paquete de constraints :

import Data.Constraint
class Differentiable (f :: * -> *) where
type D f :: * -> *
witness :: p f -> Dict (Differentiable (D f))

luego puede abrir manualmente el diccionario siempre que necesite recurse.

Esto le permitiría emplear la forma general de la solución en la respuesta de Casey, pero no hacer que el compilador (o tiempo de ejecución) gire para siempre en la inducción.