Come posso creare liste eterogenee (dette anche HLists) con elementi vincolati?

Question

Ho sperimentato l'utilizzo di famiglie di tipi per astrarre i toolkit dell'interfaccia utente. Mi sono sbloccato mentre provo a utilizzare HLists (http://homepages.cwi.nl/~ralf/HList/) per migliorare l'API.

mio API inizialmente sembrava qualcosa di simile:

{-# LANGUAGE TypeFamilies #-} 

class UITK tk where 
    data UI tk :: * -> * 

    stringEntry :: (UITK tk) => UI tk String 
    intEntry :: (UITK tk) => UI tk Int 

    tuple2UI :: (UI tk a,UI tk b) -> (UI tk (a,b)) 
    tuple3UI :: (UI tk a,UI tk b,UI tk c) -> (UI tk (a,b,c)) 
    tuple4UI :: (UI tk a,UI tk b,UI tk c,UI tk d) -> (UI tk (a,b,c,d)) 

ui :: (UITK tk) => (UI tk (String,Int)) 
ui = tuple2UI (stringEntry,intEntry) 

questo funziona, ma il combinatore interfaccia utente lavora su tuple, e quindi ho bisogno di una funzione diversa per ogni dimensione tupla. Pensavo di poter usare qualcosa come HLists, ma o non è possibile, (o si spera) mi manca solo il tipo-fu necessario.

Ecco il mio tentativo:

{-# LANGUAGE TypeFamilies,FlexibleInstances,MultiParamTypeClasses #-} 

-- A heterogeneous list type 

data HNil = HNil deriving (Eq,Show,Read) 
data HCons e l = HCons e l deriving (Eq,Show,Read) 

-- A list of UI fields, of arbitrary type, but constrained on their 
-- tk parameter. The StructV associated type captures the return 
-- type of the combined UI 

class (UITK tk) => FieldList tk l 
    where type StructV tk l 

instance (UITK tk) => FieldList tk HNil 
    where type StructV tk HNil = HNil 

instance (UITK tk, FieldList tk l) => FieldList tk (HCons (UI tk a) l) 
    where type StructV tk (HCons (UI tk a) l) = (HCons a (StructV tk l)) 

fcons :: (UITK tk, FieldList tk l) => UI tk a -> l -> HCons (UI tk a) l 
fcons = HCons 

-- Now the abstract ui toolkit definition 

class UITK tk where 
    data UI tk :: * -> * 

    stringEntry :: (UITK tk) => UI tk String 
    intEntry :: (UITK tk) => UI tk Int 

    structUI :: (FieldList tk l) => l -> (UI tk (StructV tk l)) 

-- this doesn't work :-(

ui :: (UITK tk) => (UI tk (HCons String (HCons Int HNil))) 
ui = structUI (fcons stringEntry 
       (fcons intEntry 
       HNil)) 

La definizione alla fine mi dà parecchi errori, il primo dei quali è:

Z.hs:38:6: 
    Could not deduce (FieldList 
         tk (HCons (UI tk0 String) (HCons (UI tk1 Int) HNil))) 
     arising from a use of `structUI' 
    from the context (UITK tk) 
     bound by the type signature for 
       ui :: UITK tk => UI tk (HCons String (HCons Int HNil)) 
     at Z.hs:(38,1)-(40,21) 
    Possible fix: 
     add (FieldList 
      tk 
      (HCons 
       (UI tk0 String) (HCons (UI tk1 Int) HNil))) to the context of 
     the type signature for 
      ui :: UITK tk => UI tk (HCons String (HCons Int HNil)) 
     or add an instance declaration for 
     (FieldList tk (HCons (UI tk0 String) (HCons (UI tk1 Int) HNil))) 
    In the expression: 
     structUI (fcons stringEntry (fcons intEntry HNil)) 
    In an equation for `ui': 
     ui = structUI (fcons stringEntry (fcons intEntry HNil)) 

Senza completamente la comprensione di questo, penso di poter vedere almeno uno dei problemi Non sto informando con successo il compilatore che i 3 tipi di parametri di tk sono tutti dello stesso tipo (cioè si riferisce a tk, tk0, tk1) sopra. Non lo capisco - il mio costruttore di fcons ha lo scopo di mantenere i parametri tk dell'interfaccia utente coerenti per l'HList costruito.

Questa è la mia prima esperienza con le famiglie di tipi e classi di tipi a più parametri, quindi è probabile che manchi qualcosa di fondamentale.

È possibile costruire elenchi eterogenei con elementi vincolati? Dove sto andando male?

Answer 1

L'errore di tipo è da questa catena di logica: il 'ui' ha 'structui' più esterno e 'structUI :: (FieldList tk l) =>' ha bisogno del '(FieldList tk l)' dove 'tk' e 'l' deve corrispondere alla firma del tipo che hai scritto per 'ui'.

Tutto è, singolarmente, polimorfico nella variabile di tipo 'tk'.

Il controllo di tipo fornisce un diverso tk0 all'argomento di structui/fcons e solo perché si dispone di un'istanza con la corrispondenza di tk non significa che non arriverò e creare un'istanza FieldList con distinti tk. Quindi il controllo del tipo è bloccato.

Ecco come posso risolvere questo problema per il tipo di controllo:

-- Use this instance instead of the one you wrote 
instance (UITK tk, FieldList tk l, tk ~ tk') => FieldList tk (HCons (UI tk' a) l) 
    where type StructV tk (HCons (UI tk' a) l) = (HCons a (StructV tk l)) 

-- Now this works :) 
ui :: (UITK tk) => (UI tk (HCons String (HCons Int HNil))) 
ui = structUI (fcons stringEntry 
       (fcons intEntry 
       HNil)) 

L'istanza di sostituzione rispetta tutte le possibili combinazioni di TK e tk', quindi richiede che siano la stessa cosa. Nessuno può venire e scrivere un'altra istanza di questo tipo senza sovrapposizioni.

risposta al commento di timbod: Considerate questo codice, si noti che (toEnum 97) :: Char è 'un'

class TwoParam a b where 
    combine :: a -> b -> (a,b) 
    combine = (,) 

instance TwoParam c c 

t1 :: (TwoParam Char b) => Char -> b -> (Char,b) 
t1 = combine 

main = print (t1 'a' (toEnum 97)) 

Questo non riesce con il messaggio:

No instance for (TwoParam Char b0) arising from a use of `t1' 
Possible fix: add an instance declaration for (TwoParam Char b0) 
In the first argument of `print', namely `(t1 'a' (toEnum 98))' 
In the expression: print (t1 'a' (toEnum 98)) 
In an equation for `main': main = print (t1 'a' (toEnum 98)) 
Failed, modules loaded: none. 

Perché? Il controllo del tipo deduce che (toEnum 98) ha qualche tipo di Enum, e potrebbe essere Char, ma non dedurrà che debba essere Char.Il type checker non corrisponderà (toEnum 97) a Char anche se l'unica istanza disponibile di (TwoParam Char b) richiederebbe l'abbinamento b con Char. Il compilatore è corretto qui perché ho potuto scriverà altro esempio:

-- instance TwoParam Char Integer 

Con questa seconda (sovrapposizione) istanza non è più evidente l'istanza deve essere scelto. La soluzione è quella di utilizzare quanto sopra 'trucco':

-- instance (c ~ d) => TwoParam c d 

Il tipo di controllo guarda solo al 'TwoParam c d' quando si sceglie un esempio, e questo corrisponde tutto. Poi si cerca di soddisfare il vincolo

Char ~ TypeOf (fromEnum 98)

che avrà successo. Con il trucco "main" print ('a', 'a')