edit: he seguido con una más pregunta específica. Gracias ms responden aquí, y creo que el seguimiento de la pregunta hace un mejor trabajo de explicar un poco de confusión he introducido aquí.
TL;DR estoy luchando para conseguir pruebas de restricciones en las expresiones, mientras que el uso de GADTs con existencial restricciones en la clasificación de constructores. (eso es un grave bocado, lo siento!)
He destilado un problema a la siguiente. Tengo una simple GADT que representa los puntos de llamada X y la función de las aplicaciones de llamada F. Los puntos X están obligados a ser Objects.
data GADT ix a where
X :: Object ix a => a -> GADT ix a
F :: (a -> b) -> GADT ix a -> GADT ix b
Constrained se refiere a los contenedores cuyos objetos están restringidos por algo y Object es que algo. (edit: mi problema real consiste en Category y Cartesian clases de limitado de categorías)
-- | I can constrain the values within containers of kind `* -> *`
class Constrained (ix :: * -> *) where
type Object ix a :: Constraint
-- | Here's a trivial constraint. A more interesting one might include `Typeable a`, for ex
instance Constrained (GADT ix) where
type Object (GADT ix) a = (Constrained ix, Object ix a)
Me gustaría escribir una expresión:
-- error: Could not deduce: Object ix Int arising from a use of ‘X’
ex0 :: GADT ix String
ex0 = F show (X (3 :: Int))
Y mientras que la solución obvia funciona, se vuelve rápidamente detallado cuando la construcción de grandes expresiones:
-- Typechecks, but eventually verbose
ex1 :: Object ix Int => GADT ix String
ex1 = F show (X (3 :: Int))
Creo que la solución correcta debería ser algo como esto:
-- error: Could not deduce: Object ix Int arising from a use of ‘X’
ex2 :: Constrained ix => GADT ix String
ex2 = F show (X (3 :: Int))
Pero todavía no puedo conseguir que la prueba de Object ix Int.
Estoy seguro de que es más sencillo de lo que yo estoy pensando. He intentado añadir restricciones a la Object restricción de la familia en el GADT instancia de la clase. He tratado de ofrecer las limitaciones en la expresión de la firma. He intentado QuantifiedConstraintsaunque , no estoy seguro de comprender plenamente todavía. Por favor ayuda me sabios!
Ejecutables:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE InstanceSigs #-}
module Test where
import Data.Kind
import Data.Functor.Identity
import Data.Functor.Const
-- | I can constrain the values within containers of kind `* -> *`
class Constrained (ix :: * -> *) where
type Object ix a :: Constraint
-- | Here's a trivial constraint. A more interesting one might include `Typeable a`, for instance
instance Constrained (GADT ix) where
type Object (GADT ix) a = (Constrained ix, Object ix a)
-- | A demo GADT that has function application ('F'), and points ('X'). The
-- points are constrained.
data GADT ix a where
X :: Object ix a => a -> GADT ix a
F :: (a -> b) -> GADT ix a -> GADT ix b
-- -- Broken
-- -- error: Could not deduce: Object ix Int arising from a use of ‘X’
-- ex0 :: GADT ix String
-- ex0 = F show (X (3 :: Int))
-- Typechecks
-- but for larger programs becomes verbose, requiring many explicit constraints
ex1 :: Object ix Int => GADT ix String
ex1 = F show (X (3 :: Int))
-- -- What I want, but, it's broken
-- ex2 :: Constrained ix => GADT ix String
-- ex2 = F show (X (3 :: Int))
YourFunc, que había introducir una tonelada de hasta el frente de la caldera de la placa (un nuevo preludio), aunque, probablemente eliminar futuro repetitivo. WrtInferrenceChain, Estoy luchando por mapa sobre mi problema, pero tal vez el seguimiento ayuda a explicar mejor? Gracias por cierto!