¿Cómo resuelve haskell las instancias superpuestas?

functional-dependencies type-level-computation

Question

Discúlpeme si utilizo la terminología incorrecta. Soy un principiante en la manipulación de tipos de haskell ... Estoy tratando de usar instancias superpuestas con dependencias funcionales para realizar una programación de nivel de tipo con listas HL.

Aquí mi objetivo es tratar de escribir una clase de tipos HNoNils l l'' , donde HNoNils l l'' significa que, siendo l un tipo de lista (por ejemplo: Int : String : EmptyNil : Int : HNil ), l'' es el tipo de lista correspondiente sin el tipo vacío específico EmptyNil (resultado del ejemplo: Int:String:Int:HNil ):

{-# LANGUAGE ExistentialQuantification,
  FunctionalDependencies,
  FlexibleInstances,
  UndecidableInstances,
  OverlappingInstances,
  TypeFamilies #-}

import Data.HList 
import Data.TypeLevel.Bool

--Type Equality operators
--usedto check if a type is equal to another
class TtEq a b eq | a b -> eq
instance     TtEq a a True
instance eq~False => TtEq a b eq 


data EmptyNil = EmptyNil deriving (Show) --class representing empty channel
--class intended to generate a list type with no type of EmptyNil
-- Example: HCons Int $ HCons EmptyNil HNil should give HCons Int HNil
class (HList list, HList out) => HNoNils list out | list -> out 
    where  hNoNils :: list -> out 

-- l gives l'' means (HCons EmptyNil l) gives l''
instance (HNoNils l l'',TtEq e EmptyNil True ) => HNoNils (HCons e l) l''
    where hNoNils (HCons e l) = hNoNils l

-- l gives l'' means (HCons e l) gives (HCons e l'') for all e 
instance (HNoNils l l'') => HNoNils (HCons e l) (HCons e l'')
    where hNoNils (HCons e l) = hCons e $ hNoNils l

--base case
instance  HNoNils HNil HNil
    where hNoNils _ = hNil

testList  = HCons EmptyNil $ HCons EmptyNil HNil
testList1 = HCons "Hello"  $ HCons EmptyNil HNil 
testList2 = HCons EmptyNil $ HCons "World"  HNil
testList3 = HCons "Hello"  $ HCons "World"  HNil

main:: IO ()
main = do
    print $ hNoNils testList  -- should get HNil
    print $ hNoNils testList1 -- should get HCons "Hello" HNil
    print $ hNoNils testList2 -- should get HCons "World" HNil
    print $ hNoNils testList3 -- should get HCons "Hello" (HCons "World" HNil)

Sin embargo, cuando ejecuto este código como está, todas mis llamadas a hNoNils parecen resolverse a través de la segunda declaración de instancia menos específica, lo que significa (al menos parece), que para todos l , tengo HNoNils ll .

Basado en lo que he leído, con la extensión OverlappingInstances , se supone que el sistema siempre se resuelve en la instancia más específica.

aquí

• la primera instancia tiene las restricciones (HNoNils l l'',TtEq e EmptyNil True )

• la segunda instancia tiene las restricciones HNoNils l l''

Perdóneme si me equivoco, pero parece que la primera instancia es más específica que la segunda, por lo que debería ir por esa, ¿verdad?

He intentado agregar restricciones para intentar deshacerme de la superposición, es decir, agregando la restricción de igualdad opuesta y separada a la segunda instancia:

-- l gives l'' means (HCons EmptyNil l) gives l''
instance (HNoNils l l'',TtEq e EmptyNil True ) => HNoNils (HCons e l) l''
    where hNoNils (HCons e l) = hNoNils l

-- l gives l'' means (HCons e l) gives (HCons e l'') for all e 
-- added constraint of TtEq e EmptyNil False
instance (HNoNils l l'',TtEq e EmptyNil False) => HNoNils (HCons e l) (HCons e l'')
    where hNoNils (HCons e l) = hCons e $ hNoNils l

Intenté eliminar la extensión de la instancia superpuesta aquí, y obtengo errores de superposición.

Overlapping instances for HNoNils
                                (HCons EmptyNil (HCons [Char] HNil)) (HCons EmptyNil l'')
Matching instances:
      instance (HNoNils l l'', TtEq e EmptyNil True) =>
               HNoNils (HCons e l) l''
        -- Defined at /home/raphael/Dropbox/IST/AFRP/arrow.hs:32:10
      instance (HNoNils l l'', TtEq e EmptyNil False) =>
               HNoNils (HCons e l) (HCons e l'')
        -- Defined at /home/raphael/Dropbox/IST/AFRP/arrow.hs:36:10

No entiendo el segundo partido. Después de todo, en esta resolución, tenemos e igual a EmptyNil, así que TtEq e EmptyNil True ... ¿verdad? Y, de hecho, ¿cómo llega el sistema de tipos a una situación en la que está haciendo esta pregunta? Después de todo, con las restricciones, nunca debería tener una situación del tipo HNoNils (Hcons EmptyNil l) (HCons EmptyNil l'')) , en Al menos no lo creo.

Al volver a agregar OverlappingInstances, recibo errores aún más extraños que no entiendo:

 Couldn''t match type `True'' with `False''
    When using functional dependencies to combine
      TtEq a a True,
        arising from the dependency `a b -> eq''
        in the instance declaration at /home/raphael/Dropbox/IST/AFRP/arrow.hs:23:14
      TtEq EmptyNil EmptyNil False,
        arising from a use of `hNoNils''
        at /home/raphael/Dropbox/IST/AFRP/arrow.hs:53:13-19
    In the second argument of `($)'', namely `hNoNils testList2''
    In a stmt of a ''do'' block: print $ hNoNils testList2

la segunda afirmación, TtEq EmptyNil EmptyNil False , parece decir que una llamada de función ha generado una instancia ...? Estoy un poco confundido en cuanto a de dónde vino.

Así que al tratar de resolver esto, me preguntaba:

• ¿Es posible obtener información más detallada sobre cómo funciona Haskell con las instancias? Algunas de estas combinaciones parecen imposibles. Incluso se agradecería solo un enlace a un documento que explique el mecanismo.

• ¿Existe una definición más específica de cómo funcionan las OverlappingInstances ? Siento que me estoy perdiendo algo (como tal vez el argumento de "especificidad" solo funciona con las variables de tipo j, no con el número de restricciones ...)

edición : Así que probé una de las sugerencias de CA McCann (eliminando algunas de las restricciones) a lo siguiente:

instance (HNoNils l l'') => HNoNils (HCons EmptyNil l) l''

instance (HNoNils l l'') => HNoNils (HCons e l) (HCons e l'')

instance  HNoNils HNil HNil

Hacer esto me da algunos errores de instancias superpuestas desagradables:

Overlapping instances for HNoNils
                                (HCons EmptyNil (HCons [Char] HNil)) (HCons EmptyNil l'')
      arising from a use of `hNoNils''
    Matching instances:
      instance [overlap ok] HNoNils l l'' => HNoNils (HCons EmptyNil l) l''
        -- Defined at /Users/raphael/Dropbox/IST/AFRP/arrow.hs:33:10
      instance [overlap ok] HNoNils l l'' =>
                            HNoNils (HCons e l) (HCons e l'')
        -- Defined at /Users/raphael/Dropbox/IST/AFRP/arrow.hs:37:10

Siento que el método de resolución es de arriba hacia abajo en lugar de de abajo hacia arriba (donde el sistema nunca intentaría encontrar una instancia como esta).

edición 2 : al agregar una pequeña restricción a la segunda condición, obtuve el comportamiento esperado (vea el comentario de McCann sobre su respuesta):

-- l gives l'' means (HCons EmptyNil l) gives l''
instance (HNoNils l l'') => HNoNils (HCons EmptyNil l) l''
    where hNoNils (HCons EmptyNil l) = hNoNils l

-- l gives l'' means (HCons e l) gives (HCons e l'') for all e 
instance (HNoNils l l'',r~ HCons e l'' ) => HNoNils (HCons e l) r
    where hNoNils (HCons e l) = hCons e $ hNoNils l

Aquí lo que se agrega es la r~HCons e l'' en la segunda instancia.

Answer 1

¿Es posible obtener información más detallada sobre cómo funciona Haskell con las instancias? Algunas de estas combinaciones parecen imposibles. Incluso se agradecería solo un enlace a un documento que explique el mecanismo.

Cómo Haskell trabaja con instancias es muy simple. Está tratando con múltiples extensiones de lenguaje experimental proporcionadas por GHC, por lo que la fuente principal de información es la Guía del usuario de GHC .

¿Existe una definición más específica de cómo funcionan las OverlappingInstances? Siento que me estoy perdiendo algo (como tal vez el argumento de "especificidad" solo funciona con las variables de tipo j, no con el número de restricciones ...)

Tu conjetura es correcta. En la sección de la Guía del usuario que explica las OverlappingInstances :

Cuando GHC intenta resolver, por ejemplo, la restricción C Int Bool , intenta hacer coincidir cada declaración de instancia con la restricción, mediante la instanciación del encabezado de la declaración de instancia. Por ejemplo, considere estas declaraciones:

instance context1 => C Int a     where ...  -- (A)
instance context2 => C a   Bool  where ...  -- (B)
instance context3 => C Int [a]   where ...  -- (C)
instance context4 => C Int [Int] where ...  -- (D)

Las instancias (A) y (B) coinciden con la restricción C Int Bool , pero (C) y (D) no coinciden. Al realizar la coincidencia, GHC no tiene en cuenta el contexto de la declaración de instancia ( context1 etc.).

Piense en ello como algo así como patrones contra guardias:

instanceOfC Int a | context1 Int a = ...
instanceOfC a Bool | context2 a Bool = ...

Debido a que las clases de tipos están "abiertas", no hay un orden de coincidencias bien definido, como ocurre con una función, por lo que hay restricciones en los "patrones" que coinciden con los mismos argumentos. Desarrollé más a fondo la analogía con los patrones y guardias en una respuesta anterior .

Si traducimos sus instancias a una pseudo-función a través de la analogía anterior, el resultado es algo como esto:

hNoNils (e:l) | e == EmptyNil = hNoNils l
hNoNils (e:l) = e : hNoNils l
hNoNils [] = []

Saber que los "guardias" se ignoran al elegir un "patrón" es evidente que los dos primeros patrones no se pueden distinguir.

Pero espero que te gustaría saber cómo hacer que las cosas funcionen, no solo por qué no lo hacen actualmente. (NB: no tengo un GHC a mano en este momento, así que todo esto es de memoria y no se ha probado. Es posible que me haya equivocado con algunos detalles).

Hay varias maneras de lidiar con este tipo de cosas. Probablemente, el más general es un proceso de dos pasos que consiste en usar primero las funciones de tipo en el contexto de una instancia genérica, y luego aplazar una instancia específica de una clase auxiliar que toma parámetros adicionales:

class FooConstraint a b r | a b -> r  -- some sort of type predicate


-- the "actual" type function we want
class (FooConstraint a b result, FooAux a b result c) => Foo a b c | a b -> c

-- a single maximally generic instance
instance (FooConstraint a b result, FooAux a b result c) => Foo a b c 


-- this class receives the original a and b as arguments, but also the 
-- output of the predicate FooConstraint
class FooAux a b result c | a b result -> c

-- which lets us indirectly choose instances based on a constraint
instance ( ... ) => FooAux a b True c 
-- more instances, &c.

Es una gran molestia, como puedes ver, pero a veces es todo lo que tienes.

Afortunadamente, su caso es mucho más fácil. Recuerde la traducción a una pseudo-función de arriba, ¿realmente escribiría esa función de esa manera? Por supuesto que no, porque sería más claro así:

hNoNils (EmptyNil:l) = hNoNils l
hNoNils (e:l) = e : hNoNils l
hNoNils [] = []

Ya que EmptyNil es un constructor, puedes hacer un patrón de coincidencia en él, simplificando el código y evitando una restricción Eq superflua.

Lo mismo se aplica al equivalente de nivel de tipo: reemplace el predicado de igualdad de tipo con simplemente usar EmptyNil en el encabezado de la instancia:

instance (HNoNils l l'') => HNoNils (HCons EmptyNil l) l''

instance (HNoNils l l'') => HNoNils (HCons e l) (HCons e l'')

instance  HNoNils HNil HNil

Esta versión aún fallará en una situación, que realmente no hay manera de evitarlo. Si la lista de tipos contiene variables de tipo que potencialmente podrían unificarse con EmptyNil teniendo en cuenta que las restricciones se ignoran en este punto y que GHC debe tener en cuenta las instancias arbitrarias que luego se agregarán a EmptyNil dos primeras instancias son inevitablemente ambiguas.

Los problemas de ambigüedad de este último tipo pueden evitarse en parte asegurando que todos los casos relevantes puedan distinguirse. Por ejemplo, en lugar de eliminar un tipo como EmptyNil , podría tener constructores de tipos como:

data Some a
data None

Y luego escribe una versión de catMaybes nivel de catMaybes :

class CatOptions l l''
instance (CatOptions l l'') => CatOptions (HCons None l) l''
instance (CatOptions l l'') => CatOptions (HCons (Some e) l) (HCons e l'')
instance CatOptions HNil HNil

Esto limita los problemas de ambigüedad solo a las situaciones que son verdaderamente ambiguas, en lugar de a los casos en que una lista contiene, por ejemplo, un tipo polimórfico que representa una instancia Num arbitraria.