Singletons in liste eterogenee

Question

Mi piacerebbe scrivere una funzione che analizzi una lista eterogenea. Per amor di discussione, diamo il seguente

data Rec rs where 
    Nil :: Rec '[] 
    Cons :: ty -> Rec rs -> Rec ('(name, ty) ': rs) 

class Analyze name ty where 
    analyze :: Proxy name -> ty -> Int 

L'obiettivo finale sarebbe quello di scrivere qualcosa di simile alle seguenti

class AnalyzeRec rs where 
    analyzeRec :: Rec rs -> [(String, Int)] 

instance AnalyzeRec '[] where 
    analyzeRec Nil = [] 

instance (Analyze name ty, AnalyzeRec rs) => 
      AnalyzeRec ('(name, ty) ': rs) 
    where 
    analyzeRec (Cons hd tl) = 
     let proxy = Proxy :: Proxy name 
     in (symbolVal proxy, analyze proxy hd) : analyzeRec tl 

I bit salienti è che analyzeRec utilizza la conoscenza dei vincoli istanziati ad ogni tipo e valore nel Rec. Questo meccanismo basato su classi funziona, ma è goffo e prolisso nel caso in cui si debba fare questo più e più volte (e lo faccio).

Quindi, mi piacerebbe invece sostituirlo con un meccanismo basato su singletons. Mi piacerebbe scrivere invece una funzione come

-- no type class! 
analyzeRec :: All Analyze rs => Rec rs -> [(String, Int)] 
analyzeRec rec = 
    case rec of 
    Nil -> [] 
    Cons hd tl -> withSing $ \s -> 
     (symbolVal s, analyze s hd) : analyzeRec tl 

ma questo chiaramente cade piatto in almeno alcune dimensioni.

Qual è il modo "giusto" per scrivere tale funzione su liste eterogenee utilizzando la tecnica di Singletons? C'è un modo migliore per affrontare questo problema? Cosa dovrei aspettarmi nel risolvere questo genere di cose?

(Per avere un riferimento, questo è per un clone Servo sperimentale chiamata Serv. I file in questione sono Serv.Internal.Header.Serialization e Serv.Internal.Header come sfondo. Mi piacerebbe scrivere una funzione che prende in un elenco eterogeneo di valori di intestazione tag e poi li headerEncode in un elenco di coppie effettive (ByteString, ByteString).)

Answer 1

Cercherò di presentare qui un "idiomatica" singletons soluzione (se una cosa del genere esiste anche). Preliminari:

{-# LANGUAGE 
    RankNTypes, DataKinds, PolyKinds, ConstraintKinds, GADTs, 
    TypeOperators, MultiParamTypeClasses, TypeFamilies, ScopedTypeVariables #-} 

import Data.Singletons.Prelude 
import Data.Proxy 
import GHC.Exts (Constraint) 

-- SingI constraint here for simplicity's sake 
class SingI name => Analyze (name :: Symbol) ty where 
    analyze :: Proxy name -> ty -> Int 

data Rec rs where 
    Nil :: Rec '[] 
    Cons :: ty -> Rec rs -> Rec ('(name, ty) ': rs) 

recName :: Rec ('(name, t) ': rs) -> Proxy name 
recName _ = Proxy 

abbiamo bisogno di un All c rs vincolo, ma noi dare un giro e fare c un TyFun invece una pianura a -> Constraint costruttore:

type family AllC (c :: TyFun a Constraint -> *) (rs :: [a]) :: Constraint where 
    AllC c '[]  =() 
    AllC c (x ': xs) = (c @@ x, AllC c xs) 

TyFun ci consente di astratto su costruttori di tipo e tipo famiglie e ci dà un'applicazione parziale. Ci dà quasi funzioni di livello base di prima classe con una sintassi alquanto brutta. Nota però che perdiamo necessariamente l'iniettività del costruttore. @@ è l'operatore per l'applicazione di TyFun-s. TyFun a b -> * significa che a è l'input e è l'output e il trailing -> * è solo un artefatto della codifica. Con GHC 8.0 saremo in grado di fare solo

type a ~> b = TyFun a b -> * 

E utilizzare a ~> b da allora in poi.

Siamo in grado di attuare ora un generale mappatura "di classe" over Rec:

cMapRec :: 
    forall c rs r. 
    AllC c rs => Proxy c -> (forall name t. (c @@ '(name, t)) => Proxy name -> t -> r) -> Rec rs -> [r] 
cMapRec p f Nil   = [] 
cMapRec p f r@(Cons x xs) = f (recName r) x : cMapRec p f xs 

noti che sopra c è tipo TyFun (a, *) Constraint -> *.

e quindi implementare analyzeRec:

analyzeRec :: 
    forall c rs. (c ~ UncurrySym1 (TyCon2 Analyze)) 
    => AllC c rs => Rec rs -> [(String, Int)] 
analyzeRec = cMapRec (Proxy :: Proxy c) (\p t -> (fromSing $ singByProxy p, analyze p t)) 

In primo luogo, c ~ UncurrySym1 (TyCon2 Analyze) è solo un tipo di livello let vincolante che mi permette di usare c in Proxy c come abbreviazione. (Se volessi davvero usare tutti i trucchi sporchi, aggiungerei {-# LANGUAGE PartialTypeSignatures #-} e scrivere Proxy :: _ c).

UncurrySym1 (TyCon2 Analyze) fa la stessa cosa che uncurry Analyze farebbe se Haskell avesse pieno supporto per le funzioni di livello tipo. L'ovvio vantaggio qui è che possiamo scrivere immediatamente il tipo di analyzeRec senza famiglie o classi di tipi di livello superiore extra, e usare anche AllC molto più in generale.

---

Come bonus, cerchiamo di rimuovere il vincolo SingI da Analyze, e cercare di attuare analyzeRec.

class Analyze (name :: Symbol) ty where 
    analyze :: Proxy name -> ty -> Int 

Ora dobbiamo richiedere una ulteriore vincolo che esprime che tutti i name -s nel nostro Rec sono SingI.Possiamo usare due cMapRec -s, e zip i risultati:

analyzeRec :: 
    forall analyze names rs. 
    (analyze ~ UncurrySym1 (TyCon2 Analyze), 
    names ~ (TyCon1 SingI :.$$$ FstSym0), 
    AllC analyze rs, 
    AllC names rs) 
    => Rec rs -> [(String, Int)] 
analyzeRec rc = zip 
    (cMapRec (Proxy :: Proxy names) (\p _ -> fromSing $ singByProxy p) rc) 
    (cMapRec (Proxy :: Proxy analyze) (\p t -> analyze p t) rc) 

Qui TyCon1 SingI :.$$$ FstSym0 può essere tradotto come SingI . fst.

Questo è ancora approssimativamente nel livello di astrazione che può essere prontamente espresso con TyFun-s. Il limite principale, ovviamente, è la mancanza di lambda. Idealmente non dovremmo usare zip, invece useremmo AllC (\(name, t) -> (SingI name, Analyze name t)) e usare un singolo cMapRec. Con singletons, se non siamo più in grado di utilizzarlo con la programmazione a livello di codice senza punti, dobbiamo introdurre una nuova famiglia di tipi puntuali.

In modo divertente, GHC 8.0 sarà abbastanza potente da consentire l'implementazione di lambda di livello testo da zero, anche se probabilmente sarà brutta da morire. Ad esempio, \p -> (SingI (fst p), uncurry Analyze p) potrebbe essere simile a questa:

Eval (
    Lam "p" $ 
    PairL :@@ 
     (LCon1 SingI :@@ (FstL :@@ Var "p")) :@@  
     (UncurryL :@@ LCon2 Analyze :@@ Var "p")) 

dove tutti i L suffissi indicano le immersioni termine lambda di ordinaria TyFun -s (ancora un altro insieme di abbreviazioni da generare da TH ...).

Ho un prototype, anche se funziona ancora con le variabili ancora più brutte di de Bruijn, a causa di un bug di GHC. Dispone anche di Fix e di pigrizia esplicita a livello di testo.

Answer 2

Penso che questo sia un approccio valido, è solo che .. a volte è necessario aiutare un po 'il sistema di tipi.

In primo luogo, il modo in cui si scrive il predicato All conta molto (se si riduce al momento giusto) e non si sa quale All si sta utilizzando.

Inoltre, si sta utilizzando symbolVal sul nome ma non ci sono prove che si tratti di uno KnownSymbol - è necessario aggiungere questa prova da qualche parte. L'unico posto ovvio, per me, è sulla classe tipo:

class KnownSymbol name => Analyze name ty where 
    analyze :: Proxy name -> ty -> Int 

Ecco la All predicato:

type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where 
    All c '[] =() 
    All c (x ': xs) = (c x, All c xs) 

Si noti che questa linea

analyzeRec :: All Analyze rs => Rec rs -> [(String, Int)] 

non digitare controllo (non è ben educato). Ogni elemento di rs è una tupla. Potremmo scrivere direttamente All' :: (k0 -> k1 -> Constraint) -> [(k0,k1)] -> Constraint allo stesso modo di All'. Ma è più divertente scrivere una classe tipo Uncurry:

type family Fst (x :: (k0, k1)) :: k0 where 
    Fst '(x,y) = x 

type family Snd (x :: (k0, k1)) :: k1 where 
    Snd '(x,y) = y 

class (c (Fst x) (Snd x)) => Uncurry (c :: k0 -> k1 -> Constraint) (x :: (k0, k1)) where 
instance (c x y) => Uncurry c '(x, y) 

Se questo Uncurry sembra estremamente complicato, è ancora una volta perché è importante per Uncurry c '(x,y) ridurre al c x y al momento giusto, così è scritto in un modo che forza (o meglio permette) il tipografo per ridurre questo vincolo ogni volta che lo vede.Ora la funzione è

analyzeRec :: All (Uncurry Analyze) rs => Rec rs -> [(String, Int)] 
analyzeRec r = 
    case r of 
    Nil -> [] 
    (Cons hd tl) -> let s = recName r in (symbolVal s, analyze s hd) : analyzeRec tl 

-- Helper 
recName :: Rec ('(name,ty)':rs) -> Proxy name 
recName _ = Proxy 

Questo non usa qualsiasi cosa, da singletons né ha bisogno di esso.

---

codice di lavoro completa

{-# LANGUAGE PolyKinds, ConstraintKinds, UndecidableInstances, TypeOperators #-} 
{-# LANGUAGE DataKinds, GADTs, MultiParamTypeClasses, TypeFamilies, FlexibleInstances, FlexibleContexts #-} 

import Data.Proxy 
import GHC.TypeLits 
import GHC.Prim (Constraint) 

data Rec rs where 
    Nil :: Rec '[] 
    Cons :: ty -> Rec rs -> Rec ('(name, ty) ': rs) 

class KnownSymbol name => Analyze name ty where 
    analyze :: Proxy name -> ty -> Int 

type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where 
    All c '[] =() 
    All c (x ': xs) = (c x, All c xs) 

type family Fst (x :: (k0, k1)) :: k0 where 
    Fst '(x,y) = x 

type family Snd (x :: (k0, k1)) :: k1 where 
    Snd '(x,y) = y 

class (c (Fst x) (Snd x)) => Uncurry (c :: k0 -> k1 -> Constraint) (x :: (k0, k1)) where 
instance (c x y) => Uncurry c '(x, y) 

recName :: Rec ('(name,ty)':rs) -> Proxy name 
recName _ = Proxy 

analyzeRec :: All (Uncurry Analyze) rs => Rec rs -> [(String, Int)] 
analyzeRec r = 
    case r of 
    Nil -> [] 
    (Cons hd tl) -> let s = recName r in (symbolVal s, analyze s hd) : analyzeRec tl