Sintassi di promozione dei dati

Question

Recentemente ho scoperto il Data.Promotion metà di single.Ha un sacco di famiglie di tipi che consentono calcoli essenzialmente arbitrari a livello di tipo.Ho un paio di domande sull'utilizzo:

1. Qual è la differenza tra ($), (%$), ($$), e sono correlati a :++$, :.$, eccetera?Si tratta effettivamente di operatori infissi?Ero sotto l'impressione tutti i costruttori di tipo infisso dovevano iniziare con a :.

2. Sto cercando di mappare un costruttore su un elenco:

   {-# 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 
   

   ma ho problemi con l'utilizzo di un costruttore di tipo multiparametro.Idee?

3. Sono stato in grado di sostituire tutte le funzioni di tipo che avevo scritto con funzioni equivalenti da Data.Promotion tranne questo:

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

   C'è qualche tipo di magia in corso con il Constraint tipo che ne impedirebbe la manipolazione come coppie nidificate?

Answer 1

1. Come è stato spiegato nei commenti, non esiste più un requisito sintattico per le funzioni infisse a livello di tipo che inizino con i due punti.Quindi sì, tutti questi sono operatori infissi.Non esistono due operatori infissi che siano automaticamente correlati tra loro, ma la libreria singleton utilizza internamente alcune convenzioni di denominazione, per mettere in relazione i simboli utilizzati per defunzionalizzazione (vedi sotto) alle loro controparti normali.

2. Ci sono un sacco di problemi derivanti dal fatto che le famiglie di tipi non possono essere applicate parzialmente, ma i tipi di dati sì.Ecco perché la libreria singleton utilizza una tecnica chiamata defunzionalizzazione:per ogni funzione di tipo parzialmente applicata, definisce un tipo di dati.Esiste poi una famiglia tipo (molto ampia e aperta) chiamata Apply che prende tutti questi tipi di dati che rappresentano funzioni parzialmente applicate e argomenti adatti ed esegue l'applicazione effettiva.

   Il tipo di tali rappresentazioni defunzionalizzate delle funzioni di tipo è

   TyFun k1 k2 -> *
   

   per vari motivi (a proposito, una buona introduzione a tutto questo è nel post sul blog di Richard Eisenberg "Defunzionalizzazione per la vittoria"), mentre il tipo della corrispondente funzione di tipo "normale" sarebbe

   k1 -> k2
   

   Ora tutte le funzioni di tipo di ordine superiore nei singleton si aspettano argomenti defunzionalizzati.Ad esempio, il tipo di Map È

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

   e non

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

   Ora diamo un'occhiata alle funzioni con cui stai lavorando:

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

   Il primo argomento è una funzione di tipo curry defunzionalizzata k -> k1 -> k2, e lo trasforma in una normale funzione di tipo kind k1 -> k -> k2.

   Anche:

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

   Questo è solo un sinonimo di Apply Ho menzionato sopra.

   Ora diamo un'occhiata al tuo esempio:

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

   Ci sono due problemi qui:Primo, Foo è un tipo di dati e non un simbolo defunzionalizzato come Flip si aspetta.Secondo, Flip è una famiglia di tipi e prevede tre argomenti, ma ne viene fornito solo uno.Possiamo risolvere il primo problema applicando TyCon2, che prende un tipo di dati normale e lo trasforma in un simbolo defunzionalizzato:

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

   Per il secondo problema abbiamo bisogno di una delle applicazioni parziali di Flip che i singleton già definiscono per noi:

   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 guardi da vicino, allora FlipSymN è la rappresentanza richiesta se Flip è parzialmente applicato N argomenti e Flip corrisponde all'immaginario FlipSym3.Nell'esempio, Flip viene applicato a un argomento, quindi l'esempio corretto diventa

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

   E questo funziona:

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

   Il secondo esempio è simile:

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

   Qui abbiamo i seguenti problemi:Ancora, Foo deve essere trasformato in un simbolo defunzionalizzato utilizzando TyCon2;sezioni operatore come $ b non sono disponibili a livello di tipo, da qui l'errore di analisi.Dovremo usare Flip ancora una volta, ma questa volta FlipSym2, perché lo applichiamo all'operatore $ E b.Oh, ma poi $ è parzialmente applicato, quindi abbiamo bisogno di un simbolo corrispondente a $ con 0 argomenti.Questo è disponibile come $$ nei singleton (per gli operatori simbolici, i simboli defunzionalizzati sono stati aggiunti $S).E infine, :. si applica anche parzialmente:si aspetta tre operatori, ma ne sono stati assegnati solo due.Quindi partiamo da :. A :.$$$ (tre dollari perché un dollaro corrisponde a 0, e tre dollari corrispondono a 2).Nel complesso:

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

   E ancora, funziona:

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

3. Potrei essere cieco, ma non penso che questo sia contenuto nei singleton, il che non è poi così importante ConstraintS.È una funzione utile, però.È in a libreria su cui sto attualmente lavorando.Tuttavia è ancora incompiuto e per lo più privo di documenti, ecco perché non l'ho ancora pubblicato.