Sintaxis de promoción de datos

Question

Hace poco descubrí el Data.Promotion medio de solteros.Tiene un montón de familias de tipos que permiten un cálculo esencialmente arbitrario a nivel de tipo.Tengo un par de preguntas sobre el uso:

1. Cuál es la diferencia entre ($), (%$), ($$), y ¿están relacionados con :++$, :.$, ¿etc?¿Son estos realmente operadores infijos?Era bajo la impresión todos los constructores de tipo infijo tenían que comenzar con un :.

2. Estoy intentando asignar un constructor a una lista:

   {-# LANGUAGE DataKinds, TypeOperators, PolyKinds #-}
   import Data.Promotion.Prelude
   
   data Foo a b
   type MyList = '[Int, Double, Float]
   
    -- expects one more argument to `Foo`
   type FooList1 b = Map ((Flip Foo) $ b) MyList
   
   -- parse error on the second `b`
   type FooList2 b = Map (($ b) :. Foo) MyList 
   

   pero tengo problemas para usar un constructor de tipo multiparámetro.¿Ideas?

3. Pude reemplazar todas las funciones de tipo que había escrito con funciones equivalentes de Data.Promotion excepto este:

   type family ListToConstraint (xs :: [Constraint]) :: Constraint
   type instance ListToConstraint '[] = ()
   type instance ListToConstraint (x ': xs) = (x, ListToConstraint xs)
   

   ¿Hay algún tipo de magia con el Constraint ¿tipo que evitaría su manipulación como pares anidados?

Answer 1

1. Como se explicó en los comentarios, ya no existe un requisito sintáctico para que las funciones infijas en el nivel de tipo comiencen con dos puntos.Entonces sí, todos estos son operadores infijos.No hay dos operadores infijos que se relacionen automáticamente entre sí, pero la biblioteca singletons utiliza algunas convenciones de nomenclatura internamente para relacionar los símbolos utilizados para desfuncionalización (ver más abajo) a sus contrapartes normales.

2. Hay una gran cantidad de problemas que surgen del hecho de que las familias de tipos no se pueden aplicar parcialmente, pero los tipos de datos sí.Es por eso que la biblioteca singletons utiliza una técnica llamada desfuncionalización:para cada función de tipo aplicada parcialmente, define un tipo de datos.Luego hay una familia tipográfica (muy grande y abierta) llamada Apply que toma todos estos tipos de datos que representan funciones parcialmente aplicadas y argumentos adecuados y realiza la aplicación real.

   El tipo de representaciones desfuncionalizadas de funciones de tipo es

   TyFun k1 k2 -> *
   

   por varias razones (por cierto, una buena introducción a todo esto está en la publicación del blog de Richard Eisenberg "Desfuncionalización para ganar"), mientras que el tipo de función de tipo "normal" correspondiente sería

   k1 -> k2
   

   Ahora todas las funciones de tipo de orden superior en singleton esperan argumentos desfuncionalizados.Por ejemplo, el tipo de Map es

   Map :: (TyFun k k1 -> *) -> [k] -> [k1]
   

   y no

   Map :: (k -> k1) -> [k] -> [k1]
   

   Ahora veamos las funciones con las que estás trabajando:

   Flip :: (TyFun k (TyFun k1 k2 -> *) -> *) -> k1 -> k -> k2
   

   El primer argumento es una función de curry desfuncionalizada del tipo k -> k1 -> k2, y convierte esto en una función de tipo normal de tipo k1 -> k -> k2.

   También:

   ($) :: (TyFun k1 k -> *) -> k1 -> k
   

   Esto es sólo un sinónimo de Apply Mencioné arriba.

   Ahora veamos tu ejemplo:

   type FooList1 b = Map ((Flip Foo) $ b) MyList  -- fails
   

   Hay dos problemas aquí:Primero, Foo es un tipo de datos y no un símbolo desfuncionalizado como Flip espera.Segundo, Flip es una familia de tipos y espera tres argumentos, pero solo se proporciona uno.Podemos solucionar el primer problema aplicando TyCon2, que toma un tipo de datos normal y lo convierte en un símbolo desfuncionalizado:

   TyCon2 :: (k -> k1 -> k2) -> TyFun k (TyFun k1 k2 -> *) -> *
   

   Para el segundo problema, necesitamos una de las aplicaciones parciales de Flip que singletons ya define para nosotros:

   FlipSym0 :: TyFun (TyFun k1 (TyFun k2 k -> *) -> *)
                     (TyFun k2 (TyFun k1 k -> *) -> *)
               -> *
   FlipSym1 ::    (TyFun k1 (TyFun k2 k -> *) -> *)
               -> TyFun k2 (TyFun k1 k -> *) -> *
   
   FlipSym2 ::    (TyFun k1 (TyFun k2 k -> *) -> *)
               -> k2 -> TyFun k1 k -> *
   
   Flip     ::    (TyFun k (TyFun k1 k2 -> *) -> *)
               -> k1 -> k -> k2
   

   Si miras de cerca, entonces FlipSymN ¿Es la representación requerida si Flip se aplica parcialmente a N argumentos y Flip corresponde al imaginario FlipSym3.En el ejemplo, Flip se aplica a un argumento, por lo que el ejemplo corregido se convierte en

   type FooList1 b = Map ((FlipSym1 (TyCon2 Foo)) $ b) MyList
   

   Y esto funciona:

   GHCi> :kind! FooList1 Char
   FooList1 Char :: [*]
   = '[Foo Int Char, Foo Double Char, Foo Float Char]
   

   El segundo ejemplo es similar:

   type FooList2 b = Map (($ b) :. Foo) MyList
   

   Aquí tenemos los siguientes problemas:de nuevo, Foo debe convertirse en un símbolo desfuncionalizado usando TyCon2;secciones del operador como $ b no están disponibles en el nivel de tipo, de ahí el error de análisis.Tendremos que usar Flip otra vez, pero esta vez FlipSym2, porque lo aplicamos al operador $ y b.Ah, pero entonces $ se aplica parcialmente, por lo que necesitamos un símbolo correspondiente a $ con 0 argumentos.Esto está disponible como $$ en singletons (para operadores simbólicos, los símbolos desfuncionalizados se han agregado $s).Y finalmente, :. También se aplica parcialmente:espera tres operadores, pero sólo le han dado dos.Así que pasamos de :. a :.$$$ (tres dólares porque un dólar corresponde a 0, y tres dólares corresponden a 2).Considerándolo todo:

   type FooList2 b = Map ((FlipSym2 ($$) b) :.$$$ TyCon2 Foo) MyList
   

   Y nuevamente, esto funciona:

   GHCi> :kind! FooList2 Char
   FooList2 Char :: [*]
   = '[Foo Int Char, Foo Double Char, Foo Float Char]
   

3. Puede que sea ciego, pero no creo que esto esté contenido en singletons, lo cual no tiene mucho que ver con Constraints.Sin embargo, es una función útil.esta en un biblioteca en la que estoy trabajando actualmente.Aún está inacabado y en su mayor parte indocumentado, por eso no lo he publicado todavía.