Vincolare i costruttori in una firma

Question

Quindi, sto lavorando ad un divertente esperimento in senso contestuale e sto correndo contro un muro. Sto provando a definire un tipo di dati che può essere una primitiva o una funzione che si trasforma da un costruttore all'altro.

data WeaponPart = 
    WInt Int | 
    WHash (Map.Map String Int) | 
    WNull | 
    WTrans (WeaponPart -> WeaponPart) 

instance Show WeaponPart where 
    show (WInt x) = "WInt " ++ (show x) 
    show (WHash x) = "WHash " ++ (show x) 
    show (WTrans _) = "WTrans" 
    show WNull = "WNull" 

cold :: WeaponPart -> WeaponPart 
cold (WInt x) = WHash (Map.singleton "frost" x) 
cold (WHash x) = WHash $ Map.insertWith (+) "frost" 5 x 
cold (WTrans x) = cold $ x (WInt 5) 
cold (WNull) = cold $ (WInt 5) 

ofTheAbyss :: WeaponPart -> WeaponPart 
ofTheAbyss (WTrans x) = x (WTrans x) 

Il problema è che la firma per ofTheAbyss permette a qualsiasi WeaponPart come argomento, mentre io solo voglio permettere argomenti Wtrans-constructred. Puoi vedere che ho solo scritto una corrispondenza di modello per quel caso.

Ho provato a fare con GADT ma temo fosse una tana di coniglio. Non sono mai riuscito a convincerli a fare ciò che volevo. Qualcuno ha qualche idea su come applicare solo gli argomenti di WTrans a TheAbyss? O mi manca solo qualcosa.

Grazie.

migliore, Erik

Answer 1

È possibile fare questo genere di cose con GADTs. Lungi da me giudicare se quello che risulta è una tana di coniglio, ma lasciami almeno mostrare la ricetta. Sto usando la nuova estensione PolyKinds, ma puoi gestirla con meno.

In primo luogo, decidere di quale tipo di materiale è necessario e definire un tipo di dati di questo tipo.

data Sort = Base | Compound 

Successivamente, definire i dati indicizzati in base al tipo. È come costruire un piccolo linguaggio tipizzato.

data WeaponPart :: Sort -> * where 
    WInt :: Int ->         WeaponPart Base 
    WHash :: Map.Map String Int ->     WeaponPart Base 
    WNull ::           WeaponPart Base 
    WTrans :: (Some WeaponPart -> Some WeaponPart) -> WeaponPart Compound 

È possibile rappresentare ‘ dati di qualsiasi tipo ’ tramite la quantificazione esistenziale, come segue:

data Some p where 
    Wit :: p x -> Some p 

Si noti che il x non sfugge, ma possiamo ancora esaminare le prove ‘ ’ che x ‘ soddisfa ’ p. Si noti che Some deve essere un tipo data, non uno newtype come oggetti GHC per oggetti esistenziali newtype s.

Ora sei libero di scrivere Sort -generico operazioni.Se si dispone di input generici, è possibile utilizzare solo il polimorfismo, in modo efficace currying Some p -> ... come forall x. p x -> ....

instance Show (WeaponPart x) where 
    show (WInt x) = "WInt " ++ (show x) 
    show (WHash x) = "WHash " ++ (show x) 
    show (WTrans _) = "WTrans" 
    show WNull  = "WNull" 

L'esistenziale è necessario per Sort uscite -generic: qui lo uso per ingresso e uscita.

cold :: Some WeaponPart -> Some WeaponPart 
cold (Wit (WInt x)) = Wit (WHash (Map.singleton "frost" x)) 
cold (Wit (WHash x)) = Wit (WHash $ Map.insertWith (+) "frost" 5 x) 
cold (Wit (WTrans x)) = cold $ x (Wit (WInt 5)) 
cold (Wit WNull)  = cold $ Wit (WInt 5) 

ho dovuto aggiungere il tocco occasionale di Wit circa il posto, ma è lo stesso programma.

Nel frattempo, possiamo ora scrivere

ofTheAbyss :: WeaponPart Compound -> Some WeaponPart 
ofTheAbyss (WTrans x) = x (Wit (WTrans x)) 

Quindi non è orrenda di lavorare con sistemi di tipo embedded. Qualche volta c'è un costo: se vuoi che la tua lingua incorporata abbia subsorting, potresti scoprire di fare calcoli extra solo per cambiare l'indice del tipo di alcuni dati, senza fare alcuna differenza con i dati stessi. Se non hai bisogno di interruzione, la disciplina in più può spesso essere un vero amico.

Answer 2

Si sta cercando di limitare la vostra funzione non per tipo, ma per il costruttore. Questa non è una cosa fattibile.

In effetti, non dovrebbe essere una cosa fattibile - se stai scrivendo un'altra funzione, e hai qualche sconosciuto WeaponPart, devi essere in grado di passarlo a ofTheAbyss o no - che deve tipografare o non.

Le due opzioni mi vengono in mente sono:

a) Dare ofTheAbyss tipo (WeaponPart -> WeaponPart) -> WeaponPart, "spacchettamento" del costruttore.

b) Avere ofTheAbyss dare un errore di runtime su qualsiasi altro costruttore.

ofTheAbyss :: WeaponPart -> WeaponPart 
ofTheAbyss (WTrans x) = x (WTrans x) 
ofTheAbyss _ = error "Illegal argument to ofTheAbyss was not a WTrans" 

Answer 3

Ecco un'altra possibile soluzione: dividere il tipo di dati in due. Ho usato nomi coerenti con altre risposte per rendere più facile vedere i paralleli.

data WeaponPartBase 
    = WInt Int 
    | WHash (Map.Map String Int) 
    | WNull 

data WeaponPartCompound = WTrans (WeaponPart -> WeaponPart) 
data WeaponPart = Base WeaponPartBase | Compound WeaponPartCompound 

cold :: WeaponPart -> WeaponPart 
cold (Base (WInt x)) = Base (WHash (Map.singleton "frost" x)) 
cold (Base (WHash x)) = Base (WHash $ Map.insertWith (+) "frost" 5 x) 
cold (Base WNull) = cold (Base (WInt 5)) 
cold (Compound (WTrans x)) = cold (x (Base (WInt 5)) 

ofTheAbyss :: WeaponPartCompound -> WeaponPart 
ofTheAbyss (WTrans x) = x (WCompound (WTrans x)) 

Questo può essere reso leggermente più conveniente dichiarando una classe per le cose fondamentali:

class Basic a where 
    wint :: Int -> a 
    whash :: Map.Map String Int -> a 
    wnull :: a 

class Compounded a where 
    wtrans :: (WeaponPart -> WeaponPart) -> a 

instance Basic WeaponPartBase where 
    wint = WInt 
    whash = WHash 
    wnull = WNull 

instance Basic WeaponPart where 
    wint = Base . wint 
    whash = Base . whash 
    wnull = Base wnull 

instance Compounded WeaponPartCompound where 
    wtrans = WTrans 

instance Compounded WeaponPartCompound where 
    wtrans = Compound . wtrans 

modo che ad esempio cold e ofTheAbyss potrebbe apparire come questo, invece:

cold' (Base (WInt x)) = whash (Map.singleton "frost" x) 
cold' (Base (WHash x)) = whash $ Map.insertWith (+) "frost" 5 x 
cold' (Base WNull) = cold' (wint 5) 
cold' (Compound (WTrans x)) = cold' (x (wint 5)) 

ofTheAbyss' (WTrans x) = x (wtrans x)