haskell - Técnicas para trazar restricciones

constraints ghc

Question

Aquí está el escenario: he escrito algún código con una firma de tipo y las quejas de GHC no pudieron deducir x ~ y para algunos y . Por lo general, puede lanzar un hueso de GHC y simplemente agregar el isomorfismo a las restricciones de función, pero esta es una mala idea por varias razones:

1. No enfatiza la comprensión del código.
2. Puede terminar con 5 restricciones donde una hubiera bastado (por ejemplo, si las 5 están implícitas en una restricción más específica)
3. Puede terminar con restricciones falsas si ha hecho algo mal o si GHC no es útil.

Acabo de pasar varias horas luchando contra el caso 3. Estoy jugando con syntactic-2.0 , y estaba tratando de definir una versión de dominio independiente del dominio, similar a la versión definida en NanoFeldspar.hs .

Tuve esto:

{-# LANGUAGE GADTs, FlexibleContexts, TypeOperators #-}
import Data.Syntactic
-- Based on NanoFeldspar.hs
data Let a where
Let :: Let (a :-> (a -> b) :-> Full b)
share :: (Let :<: sup,
Domain a ~ sup,
Domain b ~ sup,
SyntacticN (a -> (a -> b) -> b) fi)
=> a -> (a -> b) -> a
share = sugarSym Let

y GHC could not deduce (Internal a) ~ (Internal b) , que ciertamente no es lo que buscaba. Entonces, o bien escribí un código que no tenía la intención de (que requería la restricción), o GHC quería esa restricción debido a algunas otras restricciones que había escrito.

Resulta que necesitaba agregar (Syntactic a, Syntactic b, Syntactic (a->b)) a la lista de restricciones, ninguna de las cuales implica (Internal a) ~ (Internal b) . Básicamente me topé con las restricciones correctas; Todavía no tengo una forma sistemática de encontrarlos.

Mis preguntas son:

1. ¿Por qué propuso GHC esa restricción? En ninguna parte en la sintaxis, hay una restricción Internal a ~ Internal b , ¿entonces de dónde sacó GHC eso?
2. En general, ¿qué técnicas se pueden usar para rastrear el origen de una restricción que GHC cree que necesita? Incluso para las restricciones que puedo descubrir por mí mismo, mi enfoque es esencialmente brutal, forzando el camino ofensivo al anotar físicamente las restricciones recursivas. Básicamente, este enfoque consiste en ir por un agujero infinito de restricciones y es el método menos eficiente que puedo imaginar.

Answer 1

En primer lugar, su función tiene el tipo incorrecto; Estoy bastante seguro de que debería ser (sin el contexto) a -> (a -> b) -> b . GHC 7.10 es algo más útil para señalarlo, porque con su código original, se queja de una restricción que falta Internal (a -> b) ~ (Internal a -> Internal a) . Después de corregir el tipo de share , GHC 7.10 sigue siendo útil para guiarnos:

1. Could not deduce (Internal (a -> b) ~ (Internal a -> Internal b))

2. Después de agregar lo anterior, obtenemos Could not deduce (sup ~ Domain (a -> b)) se Could not deduce (sup ~ Domain (a -> b))

3. Después de agregar eso, obtenemos Could not deduce (Syntactic a) se Could not deduce (Syntactic a) , Could not deduce (Syntactic b) y Could not deduce (Syntactic (a -> b))

4. Después de agregar estos tres, finalmente se comprueba; así que terminamos con

   share :: (Let :<: sup,
   Domain a ~ sup,
   Domain b ~ sup,
   Domain (a -> b) ~ sup,
   Internal (a -> b) ~ (Internal a -> Internal b),
   Syntactic a, Syntactic b, Syntactic (a -> b),
   SyntacticN (a -> (a -> b) -> b) fi)
   => a -> (a -> b) -> b
   share = sugarSym Let

Así que diría que GHC no ha sido inútil para guiarnos.

En cuanto a su pregunta sobre el rastreo de donde GHC obtiene sus requisitos de restricciones, puede probar los indicadores de depuración de GHC , en particular, -ddump-tc-trace , y luego leer el registro resultante para ver dónde está Internal (a -> b) ~ t y (Internal a -> Internal a) ~ t se agregan al conjunto Wanted , pero será una lectura bastante larga.