Sintaxe de promoção de dados

Question

Recentemente descobri o Data.Promotion metade de solteiros.Possui muitas famílias de tipos que permitem computação essencialmente arbitrária no nível do tipo.Tenho algumas perguntas sobre o uso:

1. Qual é a diferença entre ($), (%$), ($$), e eles estão relacionados a :++$, :.$, etc?Esses são realmente operadores infixos?Eu era sob a impressão todos os construtores do tipo infix tiveram que começar com um :.

2. Estou tentando mapear um construtor em uma 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 
   

   mas estou tendo problemas para usar um construtor do tipo multiparâmetro.Ideias?

3. Consegui substituir todas as funções de tipo que escrevi por funções equivalentes de Data.Promotion exceto este:

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

   Existe algum tipo de magia acontecendo com o Constraint tipo que impediria sua manipulação como pares aninhados?

Answer 1

1. Como foi explicado nos comentários, não há mais um requisito sintático para que funções infixas no nível de tipo comecem com dois pontos.Então sim, todos esses são operadores infixos.Não existem dois operadores infixos automaticamente relacionados entre si, mas a biblioteca singletons usa algumas convenções de nomenclatura internamente para relacionar símbolos usados ​​para desfuncionalização (veja abaixo) para suas contrapartes normais.

2. Há vários problemas decorrentes do fato de que as famílias de tipos não podem ser parcialmente aplicadas, mas os tipos de dados podem.É por isso que a biblioteca singletons usa uma técnica chamada desfuncionalização:para cada função de tipo parcialmente aplicada, define um tipo de dados.Existe então uma família de tipos (muito grande e aberta) chamada Apply que pega todos esses tipos de dados que representam funções parcialmente aplicadas e argumentos adequados e executa a aplicação real.

   O tipo de tais representações desfuncionalizadas de funções de tipo é

   TyFun k1 k2 -> *
   

   por vários motivos (aliás, uma boa introdução a tudo isso está na postagem do blog de Richard Eisenberg “Desfuncionalização para a vitória”), enquanto o tipo da função do tipo "normal" correspondente seria

   k1 -> k2
   

   Agora, todas as funções de tipo de ordem superior em singletons esperam argumentos desfuncionalizados.Por exemplo, o tipo de Map é

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

   e não

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

   Agora vamos dar uma olhada nas funções com as quais você está trabalhando:

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

   O primeiro argumento é uma função curry desfuncionalizada do tipo k -> k1 -> k2, e transforma isso em uma função de tipo normal do tipo k1 -> k -> k2.

   Também:

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

   Este é apenas um sinônimo para o Apply Eu mencionei acima.

   Agora vamos ver seu exemplo:

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

   Existem dois problemas aqui:Primeiro, Foo é um tipo de dados e não um símbolo desfuncionalizado como Flip espera.Segundo, Flip é uma família de tipos e espera três argumentos, mas apenas um é fornecido.Podemos resolver o primeiro problema aplicando TyCon2, que pega um tipo de dados normal e o transforma em um símbolo desfuncionalizado:

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

   Para o segundo problema, precisamos de uma das aplicações parciais de Flip que singletons já define para nós:

   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
   

   Se você olhar de perto, então FlipSymN é a representação necessária se Flip é parcialmente aplicado N argumentos, e Flip corresponde ao imaginário FlipSym3.No exemplo, Flip é aplicado a um argumento, então o exemplo corrigido se torna

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

   E isso funciona:

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

   O segundo exemplo é semelhante:

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

   Aqui temos os seguintes problemas:de novo, Foo deve ser transformado em um símbolo desfuncionalizado usando TyCon2;seções do operador, como $ b não estão disponíveis no nível do tipo, daí o erro de análise.Teremos que usar Flip de novo, mas desta vez FlipSym2, porque o aplicamos ao operador $ e b.Ah, mas então $ é parcialmente aplicado, então precisamos de um símbolo correspondente a $ com 0 argumentos.Isto está disponível como $$ em singletons (para operadores simbólicos, os símbolos desfuncionalizados foram anexados $e).E finalmente, :. também é parcialmente aplicado:espera três operadores, mas recebeu apenas dois.Então vamos de :. para :.$$$ (três dólares porque um dólar corresponde a 0, e três dólares correspondem a 2).Contudo:

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

   E novamente, isso funciona:

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

3. Posso ser cego, mas não acho que isso esteja contido nos singletons, que não estão muito preocupados com ConstraintS.É uma função útil, no entanto.Está em um biblioteca na qual estou trabalhando atualmente.Ainda está inacabado e em grande parte sem documentação, por isso ainda não o lancei.