Статическая гарантия по ключевым/ценностным отношениям в Data.Map
Я хочу создать специальный интеллектуальный конструктор для Data.Map с определенным ограничением на типы отношений пары ключ/значение. Это ограничение, которое я пытался выразить:
{-# 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)
для каждого поля, существует только один тип значения, с которым он должен быть связан. В моем случае для поля Speed
не имеет смысла отображать a ByteString
. Поле A Speed
должно однозначно отображать a Float
Но я получаю следующую ошибку типа:
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)'
с помощью -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'
Я понимаю, почему я получаю неправильное совпадение вида, но как я могу выразить это ограничение, так что это ошибка времени компиляции, чтобы использовать toPair
для несоответствия Field
и Value
.
Мне предложили #haskell использовать GADT
, но я еще не смог это выяснить.
Цель состоит в том, чтобы иметь возможность писать
type Record = Map Field Value
mkRecord :: [Field] -> [Value] -> Record
mkRecord = (fromList .) . zipWith toPair
чтобы я мог сделать безопасным Map
, где соблюдаются инварианты ключа/значения.
Итак, это должно проверять тип
test1 = mkRecord [Speed, ID] [VFloat 1.0, VInt 2]
но это должна быть ошибка времени компиляции
test2 = mkRecord [Speed] [VInt 1]
EDIT:
Я начинаю думать, что мои конкретные требования невозможны. Используя мой оригинальный пример
data Foo = FooInt | FooFloat
data Bar = BarInt Int | BarFloat Float
Чтобы обеспечить ограничение на Foo
и Bar
, должен быть какой-то способ разграничения между FooInt
и FooFloat
на уровне типа и аналогичным образом для Bar
. Таким образом, мне вместо этого нужны два GADT
data Foo :: * -> * where
FooInt :: Foo Int
FooFloat :: Foo Float
data Bar :: * -> * where
BarInt :: Int -> Bar Int
BarFloat :: Float -> Bar Float
теперь я могу написать экземпляр для Pair
, который выполняется только тогда, когда теги Foo
и Bar
отмечены тем же типом
instance Pair (Foo a) (Bar a)
и у меня есть свойства, которые я хочу
test1 = toPair FooInt (BarInt 1) -- type-checks
test2 = toPair FooInt (BarFloat 1) -- no instance for Pair (Foo Int) (Bar Float)
но я теряю возможность писать xs = [FooInt, FooFloat]
, потому что для этого потребуется гетерогенный список. Более того, если я попытаюсь сделать синоним Map
type FooBar = Map (Foo ?) (Bar ?)
, я застрял с Map
только типов Int
или только типов Float
, чего я не хочу. Это выглядит довольно безнадежным, если только у вас нет мощного колдовства типа типа, о котором я не знаю.
Ответы
Ответ 1
Версия oldschool с использованием динамических и настраиваемых и FunDeps. Чтобы это было безопасно, вам просто не нужно экспортировать абстрагирующиеся вещи, такие как конструктор SM
и класс 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
-}
Ответ 2
Вы можете использовать GADT, например,
data Bar :: * -> * where
BarInt :: Int -> Bar Int
BarFloat :: Float -> Bar Float
теперь у вас есть 2 различных типа доступных Bar (Bar Int) и (Bar Float). Тогда вы можете просто разделить Foo на 2 типа, если нет причин для этого.
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)
Это своего рода неуклюжий пример, но он показывает, как вы можете специализировать тип с помощью GADT. Идея состоит в том, что они несут тип "phantom". Это описано довольно хорошо на этой странице и с DataKinds на этой странице.
EDIT:
Если мы создадим Foo и Bar GADT, мы сможем использовать семейство типов или данных как описано здесь. Таким образом, эта комбинация позволяет нам установить тип карты на основе типа ключа. По-прежнему кажется, что есть другие, возможно, более простые способы сделать это, но он демонстрирует два больших расширения 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)
Ответ 3
Когда я впервые прочитал это, я попытался решить проблему принудительного компиляции ошибок в необходимых случаях, но что-то показалось неправильным. Затем я попробовал подход с несколькими картами и функцией подъема, но что-то все еще щеголяло. Однако, когда я понял, что по существу то, что вы пытаетесь сделать, это создать некоторую форму расширяемой записи, это напомнило мне очень классный пакет, о котором я узнал несколько месяцев назад: Виниловый пакет (доступен в Hackage). Это может быть или не быть именно тем эффектом, которым вы были, и для этого требуется GHC 7.6, но вот пример, адаптированный из readme
{-# LANGUAGE DataKinds, TypeOperators #-}
{-# LANGUAGE FlexibleContexts, NoMonomorphismRestriction #-}
import Data.Vinyl
speed = Field :: "speed" ::: Float
name = Field :: "name" ::: String
iD = Field :: "id" ::: Int
Теперь можно сделать запись, содержащую любое количество этих полей:
test1 = speed =: 0.2
test2 = speed =: 0.2
<+> name =: "Ted"
<+> iD =: 1
Это разные типы, поэтому попытка передать неправильный объем информации в заданной функции вызовет ошибку компиляции. Синоним типа может упростить его использование, но аннотации типов не требуются.
type Entity = Rec ["speed" ::: Float, "name" ::: String, "id" ::: Int]
test2 :: Entity
Библиотека предоставляет автоматические линзы на этих типах без необходимости в Template Haskell и функцию литья, которая позволяет легко обрабатывать подтипы. Например:
test2Casted :: Rec '["speed" ::: Float]
test2Casted = cast test2
(Дополнительный тик необходим, чтобы получить правильный вид для отдельной записи поля).
Это не позволяет указать точный тип для mkRecord
, который вам нужен, но он, похоже, фиксирует требования к статической проверке расширяемых записей. Если это не сработает для вас, вы, тем не менее, сможете использовать методы умного типа, найденные в источнике винила, чтобы добраться туда, куда вы хотите пойти.
Ответ 4
Я бы сделал непрозрачный тип данных с некоторыми геттерами и сеттерами.
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 }