Pattern Matching sui Tipi Promosso

Question

Possiamo scrivere singoli, le istanze complete per i parametri di tipo *:

class MyClass d where 
    f :: d -> Int 

instance MyClass (Maybe d) where 
    f _ = 3 

test1 :: Maybe d -> Int 
test1 x = f x 

Questo compila bene, e notare che non abbiamo bisogno di un (MyClass (forse d)) vincolo test1 perché il compilatore trova un'istanza corrispondente per qualsiasi Maybe d.

Possiamo anche scrivere un'istanza onnicomprensiva per i parametri di classe che sono costruttori di tipo:

class MyClass2 (a :: * -> *) where 
    g :: Tagged (a Int) Int 

instance MyClass2 a where 
    g = Tagged 3 

test2 :: Int 
test2 = untag (g :: Tagged (Maybe Int) Int) 

Questo compila anche bene, e test2 non ha bisogno di una (MyClass2 forse) vincolo, perché il compilatore trova un istanza corrispondente.

Si consideri il seguente codice giocattolo per calcolare la lunghezza di un (promosso) tipo di elenco:

{-# LANGUAGE TypeOperators, 
DataKinds, 
KindSignatures, 
GADTs, 
FlexibleInstances, 
FlexibleContexts, 
ScopedTypeVariables #-} 

import Data.Tagged 
import Data.Proxy 

data HList :: [*] -> * where 
       HNil :: HList '[] 
       HCons :: a -> HList as -> HList (a ': as) 

class ListLen a where 
    len :: Tagged a Int 

instance ListLen (HList '[]) where 
    len = Tagged 0 

instance (ListLen (HList as)) => ListLen (HList (a ': as)) where 
    len = Tagged (1+(untag (len :: Tagged (HList as) Int))) 

test3 :: Int 
test3 = untag (len :: Tagged (HList '[Int, Double, Integer]) Int) 

test4 :: (Proxy (HList qs)) -> Int 
test4 (_ :: Proxy (HList qs)) = untag (len :: Tagged (HList qs) Int) -- error occurs here 

Ciò genera l'errore:

No instance for (ListLen (HList qs)) 
     arising from a use of `len' 
    Possible fix: add an instance declaration for (ListLen (HList qs)) 
    ... 

Se si commentano la firma per test4, GHCi deduce il tipo come

test4 :: (ListLen (HList qs)) => (Proxy (HList qs)) -> Int 

ma questo non dovrebbe essere necessario. Chiaramente, ho scritto istanze per ListLen che corrispondono a qualsiasi tipo di elenco concepibile: un caso di 'lista vuota' e un caso 'contro'. Il problema rimane lo stesso se cambio il tipo del parametro ListLen per avere il tipo [*] (ad esempio, rimuovere il wrapper HList in ListLen e le sue istanze).

Se si commentano fuori test4, test3 compila e funziona bene: da quando sono (essenzialmente) dato sintassi esplicita ('[Int,Double,Integer]) per come ho costruito la lista tipo, il compilatore è stato in grado di trovare le istanze corrispondenti.

Sto tentando di scrivere codice che crea un elenco di tipi per me, quindi non dovrò scrivere la sintassi esplicita della lista di tipi. Tuttavia, sembra che l'uso della sintassi esplicita sia l'unico modo in cui GHC è in grado di abbinare queste istanze complete. Forse c'è un caso che mi manca? Sintassi che non sto usando?

Cosa posso fare per far capire a GHC che ho un'istanza per tutto il genere [*]? Sto usando GHC 7.4.2. Questo potrebbe essere essere correlato a un previous post sulla decostruzione di tipi non promossi. È possibile trovare la promozione del tipo su here.

Answer 1

Questo non è esattamente quello che vuoi, ma si avvicina molto.Ho cominciato con

data Proxy a where 
    Proxy :: ListLen a => Proxy 

poi

data Proxy a where 
    Proxy :: Tagged a Int -> Proxy a 

conseguente

test4 :: (Proxy (HList qs)) -> Int 
test4 (Proxy len) = untag len 

Il problema che è sia bisogno di avere il vincolo, o hanno Proxy contenere prove della classe richiesta (anche sebbene le istanze esistano per tutti i tipi disponibili). Qui, il metodo di classe è appena incluso in Proxy.

Un'opzione completamente diversa è semplicemente non utilizzare una classe di tipo e implementare len nel modo consueto (trascritto da Data.List.length).

len :: HList a -> Int 
len l = len' l 0 
    where 
    len' :: HList a -> Int -> Int 
    len' HNil a = a 
    len' (HCons _ xs) a = len' xs $! a + 1