Constricción de constructores en una firma

Question

Por lo tanto, estoy trabajando en un experimento divertido en el sentido contextual y estoy corriendo en una pared. Estoy tratando de definir un tipo de datos que puede ser una primitiva o una función que se transforma de un constructor a otro.

data WeaponPart = 
    WInt Int | 
    WHash (Map.Map String Int) | 
    WNull | 
    WTrans (WeaponPart -> WeaponPart) 

instance Show WeaponPart where 
    show (WInt x) = "WInt " ++ (show x) 
    show (WHash x) = "WHash " ++ (show x) 
    show (WTrans _) = "WTrans" 
    show WNull = "WNull" 

cold :: WeaponPart -> WeaponPart 
cold (WInt x) = WHash (Map.singleton "frost" x) 
cold (WHash x) = WHash $ Map.insertWith (+) "frost" 5 x 
cold (WTrans x) = cold $ x (WInt 5) 
cold (WNull) = cold $ (WInt 5) 

ofTheAbyss :: WeaponPart -> WeaponPart 
ofTheAbyss (WTrans x) = x (WTrans x) 

los problemas es que la firma de ofTheAbyss permite a cualquier WeaponPart como argumento, mientras que sólo quiero permitir que argumentos Wtrans-fabricarse de manera. Puedes ver que solo he escrito una coincidencia de patrón para ese caso.

He intentado hacer con GADT pero me temo que era un agujero de conejo. Nunca podría hacer que hagan lo que yo quería. ¿Alguien tiene alguna idea de cómo podría aplicar solo argumentos de WTrans en TheAbyss? O simplemente me estoy perdiendo algo por completo.

Gracias.

mejor, Erik

Answer 1

Usted puede hacer este tipo de cosas con GADTs. Lejos de mí es juzgar si el resultado es un agujero de conejo, pero permítanme al menos mostrar la receta. Estoy usando la nueva extensión PolyKinds, pero puede administrar con menos.

Primero, decida qué tipo de cosas necesitará y defina un tipo de datos de ese tipo.

data Sort = Base | Compound 

A continuación, defina sus datos indexados por su género. Es como construir un pequeño lenguaje escrito a máquina.

data WeaponPart :: Sort -> * where 
    WInt :: Int ->         WeaponPart Base 
    WHash :: Map.Map String Int ->     WeaponPart Base 
    WNull ::           WeaponPart Base 
    WTrans :: (Some WeaponPart -> Some WeaponPart) -> WeaponPart Compound 

Puede representar ‘ de datos de cualquier tipo ’ a través de la cuantificación existencial, de la siguiente manera:

data Some p where 
    Wit :: p x -> Some p 

Tenga en cuenta que la x no se escapa, pero todavía puede inspeccionar la evidencia ‘ ’ que x ‘ satisface ’ p. Tenga en cuenta que Some debe ser un tipo data, no un newtype ya que GHC se opone a los newtype existenciales.

Ahora puede escribir Sort -generic operations.Si tiene entradas genéricas, puede usar polimorfismo, currying efectivamente Some p -> ... como forall x. p x -> ....

instance Show (WeaponPart x) where 
    show (WInt x) = "WInt " ++ (show x) 
    show (WHash x) = "WHash " ++ (show x) 
    show (WTrans _) = "WTrans" 
    show WNull  = "WNull" 

La existencial se necesita para Sort salidas -generic: aquí lo uso para entrada y salida.

cold :: Some WeaponPart -> Some WeaponPart 
cold (Wit (WInt x)) = Wit (WHash (Map.singleton "frost" x)) 
cold (Wit (WHash x)) = Wit (WHash $ Map.insertWith (+) "frost" 5 x) 
cold (Wit (WTrans x)) = cold $ x (Wit (WInt 5)) 
cold (Wit WNull)  = cold $ Wit (WInt 5) 

he tenido que añadir el toque ocasional de Wit sobre el lugar, pero es el mismo programa.

Mientras tanto, ahora podemos escribir

ofTheAbyss :: WeaponPart Compound -> Some WeaponPart 
ofTheAbyss (WTrans x) = x (Wit (WTrans x)) 

Así que no es terrible para trabajar con sistemas de tipo incrustado. A veces hay un costo: si desea que su lenguaje incrustado tenga subsorting, es posible que realice cálculos adicionales solo para cambiar el índice del tipo de datos, sin afectar los datos. Si no necesitas un hermanamiento, la disciplina extra a menudo puede ser un verdadero amigo.

Answer 2

usted está tratando de limitar su función no por tipo, sino por el constructor. Eso no es algo factible.

De hecho, no debería ser una cosa factible - si está escribiendo otra función, y tiene alguna WeaponPart desconocida, tiene que ser capaz de pasarla a ofTheAbyss o no - eso tiene que comprobar o no.

Las dos opciones que se me ocurren son:

a) Dar ofTheAbyss tipo (WeaponPart -> WeaponPart) -> WeaponPart, "desempaquetar" el constructor.

b) Tiene ofTheAbyss dar un error de tiempo de ejecución en cualquier otro constructor.

ofTheAbyss :: WeaponPart -> WeaponPart 
ofTheAbyss (WTrans x) = x (WTrans x) 
ofTheAbyss _ = error "Illegal argument to ofTheAbyss was not a WTrans" 

Answer 3

Aquí hay otra posible solución: dividir el tipo de datos en dos. He usado nombres consistentes con otras respuestas para que sea más fácil ver los paralelos.

data WeaponPartBase 
    = WInt Int 
    | WHash (Map.Map String Int) 
    | WNull 

data WeaponPartCompound = WTrans (WeaponPart -> WeaponPart) 
data WeaponPart = Base WeaponPartBase | Compound WeaponPartCompound 

cold :: WeaponPart -> WeaponPart 
cold (Base (WInt x)) = Base (WHash (Map.singleton "frost" x)) 
cold (Base (WHash x)) = Base (WHash $ Map.insertWith (+) "frost" 5 x) 
cold (Base WNull) = cold (Base (WInt 5)) 
cold (Compound (WTrans x)) = cold (x (Base (WInt 5)) 

ofTheAbyss :: WeaponPartCompound -> WeaponPart 
ofTheAbyss (WTrans x) = x (WCompound (WTrans x)) 

Esto puede hacerse ligeramente más conveniente por la que se declara una clase para las cosas básicas:

class Basic a where 
    wint :: Int -> a 
    whash :: Map.Map String Int -> a 
    wnull :: a 

class Compounded a where 
    wtrans :: (WeaponPart -> WeaponPart) -> a 

instance Basic WeaponPartBase where 
    wint = WInt 
    whash = WHash 
    wnull = WNull 

instance Basic WeaponPart where 
    wint = Base . wint 
    whash = Base . whash 
    wnull = Base wnull 

instance Compounded WeaponPartCompound where 
    wtrans = WTrans 

instance Compounded WeaponPartCompound where 
    wtrans = Compound . wtrans 

de modo que, por ejemplo, cold y ofTheAbyss puede verse como esto en su lugar:

cold' (Base (WInt x)) = whash (Map.singleton "frost" x) 
cold' (Base (WHash x)) = whash $ Map.insertWith (+) "frost" 5 x 
cold' (Base WNull) = cold' (wint 5) 
cold' (Compound (WTrans x)) = cold' (x (wint 5)) 

ofTheAbyss' (WTrans x) = x (wtrans x)