Garanzia statica sulle relazioni chiave/valore in Data.Mappa

Question

Desidero creare un costruttore intelligente speciale per Data.Map con un certo vincolo sui tipi di relazioni coppia chiave/valore. Questo è il vincolo ho cercato di esprimere:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DataKinds #-} 

data Field = Speed | Name | ID 
data Value = VFloat Float | VString ByteString | VInt Int 

class Pair f b | f -> b where 
    toPair :: f -> b -> (f, b) 
    toPair = (,) 

instance Pair Speed (VFloat f) 
instance Pair ID (VInt i) 

per ogni campo, esiste un solo tipo di valore che deve essere associato. Nel mio caso, non ha senso che un campo Speed si associ a un ByteString. Un campo Speed dovrebbe mappare unicamente ad un Float

Ma ottengo il seguente errore di tipo:

Kind mis-match 
The first argument of `Pair' should have kind `*', 
but `VInt' has kind `Value' 
In the instance declaration for `Pair Speed (VFloat f)' 

utilizzando -XKindSignatures:

class Pair (f :: Field) (b :: Value) | f -> b where 
    toPair :: f -> b -> (f, b) 
    toPair = (,) 

Kind mis-match 
Expected kind `OpenKind', but `f' has kind `Field' 
In the type `f -> b -> (f, b)' 
In the class declaration for `Pair' 

capisco perché ho ottenere il tipo mis-match, ma come posso esprimere questo vincolo in modo che sia un errore di tipo "check-up" di compilazione per utilizzare toPair su un valore non corrispondente Field e Value.

Mi è stato suggerito da #haskell di utilizzare uno GADT, ma non sono ancora riuscito a capirlo.

L'obiettivo di questo è quello di essere in grado di scrivere

type Record = Map Field Value 

mkRecord :: [Field] -> [Value] -> Record 
mkRecord = (fromList .) . zipWith toPair 

in modo che io possa fare sicuri Map s ove siano rispettate le invarianti chiave/valore.

Quindi questo dovrebbe digitare-check

test1 = mkRecord [Speed, ID] [VFloat 1.0, VInt 2] 

ma questo dovrebbe essere un errore di tempo di compilazione

test2 = mkRecord [Speed] [VInt 1] 

EDIT:

Sto cominciando a pensare che le mie esigenze specifiche aren' t possibile. Usando il mio esempio originale

data Foo = FooInt | FooFloat 
data Bar = BarInt Int | BarFloat Float 

Al fine di far rispettare il vincolo sulla Foo e Bar, ci deve essere un modo per distinguere tra un FooInt e FooFloat a livello di tipo e allo stesso modo per Bar. Così ho invece bisogno di due GADTs

data Foo :: * -> * where 
    FooInt :: Foo Int 
    FooFloat :: Foo Float 

data Bar :: * -> * where 
    BarInt :: Int -> Bar Int 
    BarFloat :: Float -> Bar Float 

ora posso scrivere un'istanza per Pair che tiene solo quando il Foo e Bar sono entrambi etichettati con lo stesso tipo

instance Pair (Foo a) (Bar a) 

e ho le proprietà che voglio

test1 = toPair FooInt (BarInt 1) -- type-checks 
test2 = toPair FooInt (BarFloat 1) -- no instance for Pair (Foo Int) (Bar Float) 

ma perdono la capacità di scrivere xs = [FooInt, FooFloat], perché ciò richiederebbe una lista eterogenea.Inoltre se provo a rendere il sinonimo Maptype FooBar = Map (Foo ?) (Bar ?) sono bloccato con uno Map di entrambi i tipi Int o solo i tipi Float, che non è quello che voglio. Sembra piuttosto senza speranza, a meno che non ci sia qualche potente stregoneria di tipo classe di cui non sono a conoscenza.

Answer 1

Una versione oldschool che utilizza Dynamic e Typeable e FunDeps. Per tenerlo al sicuro, non è necessario esportare elementi di astrazione come il costruttore SM e la classe di caratteri SMKey.

{-# LANGUAGE DeriveDataTypeable, MultiParamTypeClasses, FunctionalDependencies, TypeSynonymInstances, FlexibleInstances #-} 
module Main where 
import qualified Data.Map as M 
import Data.Dynamic 
import Data.Typeable 

data SpecialMap = SM (M.Map String Dynamic) 

emptySM = SM (M.empty) 

class (Typeable a, Typeable b) => SMKey a b | a -> b 

data Speed = Speed deriving Typeable 
data Name = Name deriving Typeable 
data ID = ID deriving Typeable 

instance SMKey Speed Float 
instance SMKey Name String 
instance SMKey ID Int 

insertSM :: SMKey k v => k -> v -> SpecialMap -> SpecialMap 
insertSM k v (SM m) = SM (M.insert (show $ typeOf k) (toDyn v) m) 

lookupSM :: SMKey k v => k -> SpecialMap -> Maybe v 
lookupSM k (SM m) = fromDynamic =<< M.lookup (show $ typeOf k) m 

-- and now lists 

newtype SMPair = SMPair {unSMPair :: (String, Dynamic)} 
toSMPair :: SMKey k v => k -> v -> SMPair 
toSMPair k v = SMPair (show $ typeOf k, toDyn v) 

fromPairList :: [SMPair] -> SpecialMap 
fromPairList = SM . M.fromList . map unSMPair 

{- 
*Main> let x = fromPairList [toSMPair Speed 1.2, toSMPair ID 34] 
*Main> lookupSM Speed x 
Just 1.2 
-} 

Answer 2

È possibile utilizzare un GADT in questo modo,

data Bar :: * -> * where 
    BarInt :: Int -> Bar Int 
    BarFloat :: Float -> Bar Float 

Ora avete 2 tipi distinti di bar a disposizione (Bar Int) e (Bar Float) .you potremmo poi basta dividere Foo in 2 tipi a meno che non ci sia una ragione per non farlo

data FooInt 
data FooFloat 

class Pair f b c| f b -> c where 
    toPair :: f -> b -> c 

instance Pair FooInt (Bar Int) (FooInt,Int) where 
    toPair a (BarInt b)= (a,b) 

Questa è una sorta di esempio goffa ma dimostra come è possibile specializzarsi il tipo utilizzando un GADT. L'idea è che portano un "tipo fantasma" lungo. E 'descritto abbastanza bene on this page e con DataKinds on this page.

EDIT:

Se facciamo sia Foo e Bar GADT di noi possono utilizzare un tipo o di dati di famiglia as described here. Quindi, questa combinazione ci consente di impostare il tipo di mappa in base al tipo di chiave. Si sente ancora come ci sono altri modi forse più semplici per realizzare questo, ma mostra 2 fantastiche estensioni GHC!

data Foo :: * -> * where 
    FooInt :: Int -> Foo Int 
    FooFloat :: Float -> Foo Float 

data Bar :: * -> * where 
    BarInt :: Int -> Bar Int 
    BarFloat :: Float -> Bar Float 

class Pair f b c| f b -> c where 
    toPair :: f -> b -> c 

instance Pair (Foo Int) (Bar Int) ((Foo Int),Int) where 
    toPair a (BarInt b)= (a,b)  


type family FooMap k :: * 

type instance FooMap (Foo Int) = Map (Foo Int) (Bar Int) 

Answer 3

Quando ho letto prima questo ho cercato di risolvere il problema di costringere gli errori di compilazione nei casi previsti, ma qualcosa sembrava sbagliato. Ho quindi provato un approccio con più mappe e una funzione di sollevamento, ma qualcosa mi stava ancora assillando. Tuttavia, quando ho capito che in sostanza quello che stai cercando di fare è creare una sorta di record estensibile, mi ha ricordato un pacchetto molto interessante di cui mi ero reso conto qualche mese fa: lo Vinyl package (disponibile on Hackage). Questo può o non può essere esattamente gli effetti che si erano dopo, e se richiede GHC 7.6, ma qui è un esempio tratto dal readme:

{-# LANGUAGE DataKinds, TypeOperators #-} 
{-# LANGUAGE FlexibleContexts, NoMonomorphismRestriction #-} 

import Data.Vinyl 

speed = Field :: "speed" ::: Float 
name = Field :: "name" ::: String 
iD = Field :: "id" ::: Int 

ora un record può essere fatta contenente un numero qualsiasi di questi campi:

test1 = speed =: 0.2 

test2 = speed =: 0.2 
    <+> name =: "Ted" 
    <+> iD =: 1 

Questi sono di diversi tipi, quindi un tentativo di superare la quantità errata di dati in una data funzione causerà un errore di compilazione. Un sinonimo di tipo può renderlo più facile da usare, ma non è necessario digitare annotazioni.

type Entity = Rec ["speed" ::: Float, "name" ::: String, "id" ::: Int] 
test2 :: Entity 

La libreria fornisce lenti automatici su questi tipi senza la necessità di Template Haskell, e una funzione di fusione che permette di sottotipi di essere gestiti con facilità. Ad esempio:

test2Casted :: Rec '["speed" ::: Float] 
test2Casted = cast test2 

(Il segno di spunta aggiuntivo è necessario per ottenere il tipo corretto per il record di campo singolo).

Questo non consente il tipo esatto per mkRecord che cercavi, ma sembra che catturi i requisiti del controllo statico dei record estensibili. Se questo non funziona per te, potresti comunque essere in grado di utilizzare le tecniche di tipo intelligente trovate nella fonte Vinyl per arrivare dove vuoi andare.

Answer 4

Farei un tipo di dati opaco con alcuni getter e setter.

module Rec (Rec, getSpeed, getName, getID, setSpeed, setName, setID, blank) where 

data Rec = R { speed :: Maybe Double; name :: Maybe String; id :: Maybe Int } 

getSpeed :: Rec -> Maybe Double 
getSpeed = speed 

setSpeed :: Double -> Rec -> Rec 
setSpeed s r = r { speed = s } 

blank = R { speed = Nothing, name = Nothing, id = Nothing }