Проблемы с EDSL, связанные с реализацией подписки на массив в Haskell
контекст
Я пытаюсь реализовать EDSL, который очень напоминает OLP IBM (язык моделирования для линейного программирования).
Код
Haskell EDSL Code
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
-- Numbers at the type level
data Peano = Zero | Successor Peano
-- Counting Vector Type. Type information contains current length
data Vector peanoNum someType where
Nil :: Vector Zero someType
(:+) :: someType
-> Vector num someType
-> Vector (Successor num) someType
infixr 5 :+
-- Generate Num-th nested types
-- For example: Iterate (S (S Z)) [] Double => [[Double]]
type family Iterate peanoNum constructor someType where
Iterate Zero cons typ = typ
Iterate (Successor pn) cons typ =
cons (Iterate pn cons typ)
-- DSL spec
data Statement =
DecisionVector [Double]
| Minimize Statement
| Iteration `Sum` Expression
| Forall Iteration Statement
| Statement :| Statement
| Constraints Statement
infixl 8 `Sum`
infixl 3 :|
data Iteration =
String `In` [Double]
| String `Ins` [String]
data Expression where
EString :: String -> Expression
EFloat :: Double -> Expression
(:?) :: Vector n Expression -> Iterate (n) [] Double -> Expression
(:*) :: Expression -> Expression -> Expression
Lt :: Expression -> Expression -> Expression
Gt :: Expression -> Expression -> Expression
Id :: String -> Expression
infixr 5 `Lt`
infixr 5 `Gt`
infixr 6 :*
infixr 7 :?
test :: Statement
test =
let rawMaterial = 205
products = ["light", "medium", "heavy"]
demand = [59, 12, 13]
processes = [1, 2]
production = [[12,16], [1,7], [4,2]]
consumption = [25, 30]
-- foo = (EId "p" :+ EId "f" :+ Nil) `Subscript` production
-- bar = (EId "p" :+ Nil) `Subscript` cost
run = []
cost = [300, 400]
in
DecisionVector run :|
Minimize
(Sum ("p" `In` processes)
((Id "p" :+ Nil) :? cost :*
(Id "p" :+ Nil) :? run)) :|
Constraints
(Sum ("p" `In` processes)
((Id "p" :+ Nil) :? consumption :*
(Id "p" :+ Nil) :? run `Lt` EFloat rawMaterial) :|
Forall ("q" `Ins` products)
(Sum ("p" `In` processes)
((Id "q" :+ Id "p" :+ Nil) :? production :*
(Id "p" :+ Nil) :? run `Gt`
(Id "q" :+ Nil) :? demand)))
instance Show Statement where
show (DecisionVector v) = show v
show (Minimize s) = "(Minimize " ++ show s ++ ")"
show (i `Sum` e) = "(" ++ show i ++ " `Sum` " ++ show e ++ ")"
show (Forall i e) = "(Forall " ++ show i ++ show e ++ ")"
show (sa :| sb) = "(" ++ show sa ++ show sb ++ ")"
show (Constraints s) = "(Constraints " ++ show s ++ ")"
instance Show Iteration where
show (str `In` d) = "(" ++ show str ++ " `In` " ++ show d ++ ")"
show (str `Ins` d) = "(" ++ show str ++ " `Ins` " ++ show d ++ ")"
instance Show Expression where
show (EString s) = "(EString " ++ show s ++ ")"
show (EFloat f) = "(EFloat " ++ show f ++ ")"
show (Lt ea eb) = "(" ++ show ea ++ " `Lt` " ++ show eb ++ ")"
show (Gt ea eb) = "(" ++ show ea ++ " `Gt` " ++ show eb ++ ")"
show (ea :* eb) = "(" ++ show ea ++ " :* " ++ show eb ++ ")"
show (Id s) = "(Id " ++ show s ++ ")"
show (vec :? dbl) = "(" ++ show vec ++ " :? " ++ "dbl" ++ ")"
instance Show (Vector p Expression) where
show (Nil) = "Nil"
show (e :+ v) = "(" ++ show e ++ " :+ " ++ show v ++ ")"
-- eval_opl :: Statement -> [Double]
Сравнение EDSL и OPL
let rawMaterial = 205
products = ["light", "medium", "heavy"]
demand = [59, 12, 13]
processes = [1, 2]
production = [[12,16], [1,7], [4,2]]
consumption = [25, 30]
-- foo = (EId "p" :+ EId "f" :+ Nil) `Subscript` production
-- bar = (EId "p" :+ Nil) `Subscript` cost
run = []
cost = [300, 400]
in
DecisionVector run :|
Minimize
(Sum ("p" `In` processes)
((Id "p" :+ Nil) :? cost :*
(Id "p" :+ Nil) :? run)) :|
Constraints
(Sum ("p" `In` processes)
((Id "p" :+ Nil) :? consumption :*
(Id "p" :+ Nil) :? run `Lt` EFloat rawMaterial) :|
Forall ("q" `Ins` products)
(Sum ("p" `In` processes)
((Id "q" :+ Id "p" :+ Nil) :? production :*
(Id "p" :+ Nil) :? run `Gt`
(Id "q" :+ Nil) :? demand)))
соответствует коду opl
float rawMaterial = 205;
{string} products = {"light","medium","heavy"};
float demand[products] = [59,12,13];
{string} processes = {"1","2"};
float production[products][processes] = [[12,16],[1,7],[4,2]];
float consumption[processes] = [25,30];
float cost[processes] = [300,400];
dvar float+ run[processes];
minimize sum (p in processes) cost[p] * run[p];
constraints {
sum (p in processes) consumption[p] * run[p] <= rawMaterial;
forall (q in products)
sum (p in processes) production[q][p] * run[p] >= demand[q];
}
Соответствующие разделы
(:?) :: Vector n Expression -> Iterate (n) [] Double -> Expression
так же как
instance Show Expression where
[...]
show (vec :? dbl) = "(" ++ show vec ++ " :? " ++ "dbl" ++ ")"
Описание проблемы
OPL использует скобки для подписки на массив, и я попытался отобразить подписки на мой EDSL, используя следующую запись
((Id "p" :+ Id "f" :+ Nil) :? consumption
что соответствует OPL в следующем смысле:
consumption[p][f]
в первом (Id "p":+ Id "f":+ Nil) создается значение типа Vector, которое содержит информацию уровня типа, касающуюся длины указанного вектора. Согласно определению конструктора:?, Вы можете видеть, что Iterate (n) [] Double, таким образом, расширится до [[Double]]. Это аккуратно работает, как и ожидалось. Однако, в свою очередь, чтобы использовать сгенерированное синтаксическое дерево, мне нужно сопоставить шаблон с фактическими значениями.
show (vec :? dbl) = "(" ++ show vec ++ " :? " ++ "dbl" ++ ")"
Проблема: приведенная выше строка работает, но я не знаю, как использовать фактические данные. Как мне соответствовать шаблону? Можно ли вообще использовать данные? Замена DBL через очевидное
(Iterate (Successor (Successor Zero)) [] Double)
не работает Я также пытался создать семейство данных, но я не мог найти способ рекурсивного создания семейства всех произвольно вложенных списков двойных:
Double
[Double]
[[Double]]
[[[Double]]]
...
2 ответа
Чтобы узнать, какое значение на самом деле хранится Iterate n [] DoubleВы должны знать некоторую информацию о n, Эта информация обычно дается индексами некоторого GADT, которые соответствуют индуктивной структуре самого индекса (обычно известного как синглтон).
Но, к счастью для вас, вы уже сохранили Nat Индекс в структуре Vector, У вас уже есть вся необходимая информация, вам просто нужно соответствовать шаблону! например
instance Show Expression where
...
show (vec :? dbl) = "(" ++ show vec ++ go vec dbl ++ ")" where
go :: Vector n x -> Iterate n [] Double -> String
go Nil a = show a
go (_ :+ n) a = "[" ++ intercalate "," (map (go n) a) ++ "]"
Обратите внимание, что в первом шаблоне тип Nil дает тебе n ~ 0 что в свою очередь дает вам Iterate 0 [] Double ~ Double (просто по определению). Во втором паттерне у вас есть n ~ k + 1 для некоторых k а также Iterate n [] Double ~ [ Iterate k [] Double ], Сопоставление с образцом на Nat позволяет просматривать индуктивную структуру семейства типов, по существу.
Каждая функция, на которой вы пишете Iterate будет выглядеть
foo :: forall n . Vector n () -> Iterate n F X -> Y -- for some X,Y
потому что вы должны иметь такое доказательство уровня значения, чтобы написать любую индуктивную функцию на Iterate, Если вам не нравится переносить эти "фиктивные" значения, вы можете сделать их неявными с помощью класса:
class KnownNat n where
isNat :: Vector n ()
instance KnownNat 'Z where isNat = Nil
instance KnownNat n => KnownNat ('S n) where isNat = () :+ isNat
но в этом случае, так как ваш AST уже содержит конкретный Vectorвам не нужно делать никакой дополнительной работы для доступа к фактическому значению индекса - просто сопоставление с шаблоном для вектора.
У вас есть несколько опций, все они равносильны кодированию глубины итерации на уровне значений, чтобы вы могли сопоставлять с ними шаблоны.
GADT
Самый простой способ сделать это - создать GADT для представления итерации приложения конструктора типа:
data IterateF peanoNum f a where
ZeroF :: a -> IterateF Zero f a
SuccessorF :: f (IterateF pn f a) -> IterateF (Successor pn) f a
instance Functor f => Functor (IterateF peanoNum f) where
fmap f (ZeroF a) = ZeroF $ f a
fmap f (SuccessorF xs) = SuccessorF $ fmap (fmap f) xs
-- There's also an Applicative instance, see Data.Functor.Compose
одиночка
Если вы привязаны к своей типовой семье, вы можете вместо этого использовать синглтон. Синглтон - это тип, населенный одним значением, с которым вы можете сопоставить шаблон, чтобы представить фактам компилятора, известным об этом типе. Ниже приведен синглтон для натуральных чисел:
{-# LANGUAGE FlexibleContexts #-}
data SPeano pn where
SZero :: SPeano Zero
SSuccessor :: Singleton (SPeano pn) => SPeano pn -> SPeano (Successor pn)
class Singleton a where
singleton :: a
instance Singleton (SPeano Zero) where
singleton = SZero
instance Singleton (SPeano s) => Singleton (SPeano (Successor s)) where
singleton = SSuccessor singleton
Проще SPeano синглтон без Singleton Тип класса эквивалентен, но эта версия не требует написания такого количества доказательств, вместо этого она захватывает их при создании преемника.
Если мы изменим IterateF GADT из предыдущего раздела, чтобы собрать те же доказательства (потому что я ленивый), мы можем преобразовать в GADT, когда у нас есть SPeano синглтон. Независимо от того, что мы можем легко конвертировать из GADT.
data IterateF peanoNum f a where
ZeroF :: a -> IterateF Zero f a
SuccessorF :: Singleton (SPeano pn) => f (IterateF pn f a) -> IterateF (Successor pn) f a
toIterateF :: Functor f => SPeano pn -> Iterate pn f a -> IterateF pn f a
toIterateF SZero a = ZeroF a
toIterateF (SSuccessor pn) xs = SuccessorF $ fmap (toIterateF pn) xs
getIterateF :: Functor f => IterateF pn f a -> Iterate pn f a
getIterateF (ZeroF a) = a
getIterateF (SuccessorF xs) = fmap getIterateF xs
Теперь мы можем легко сделать альтернативное представление для IterateF это синглтон и применение Iterate Тип семьи.
data Iterated pn f a = Iterated (SPeano pn) (Iterate pn f a)
Я ленивый и не люблю писать доказательства, которые могут быть обработаны для меня GADT, так что я просто оставлю IterateFGADT вокруг и написать функции для Iterated с точки зрения этого.
toIterated :: Functor f => IterateF pn f a -> Iterated pn f a
toIterated xs@(ZeroF _) = Iterated singleton (getIterateF xs)
toIterated xs@(SuccessorF _) = Iterated singleton (getIterateF xs)
fromIterated :: Functor f => Iterated pn f a -> IterateF pn f a
fromIterated (Iterated pn xs) = toIterateF pn xs
instance Functor f => Functor (Iterated pn f) where
fmap f = toIterated . fmap f . fromIterated
Соответствие шаблона в toIterated это ввести доказательства, собранные в конструкции SuccessorF, Если бы у нас было что-то более сложное, мы могли бы запечатлеть это в Dict
Используйте любую другую кодировку
В конкретном случае
(:?) :: Vector n Expression -> Iterate (n) [] Double -> Expression
у тебя есть Vector n который кодирует глубину итерации Iterate n [] на уровне стоимости. Вы можете сопоставить шаблон по вектору, который либо Nil или же (_ :+ xs) доказать, что Iterate n [] либо Double или список. Вы можете использовать это для простых случаев, таких как show вложенных значений, или вы можете преобразовать Vector n в другой синглтон, чтобы использовать одно из более мощных представлений из предыдущих разделов.
-- The only proof we need to write by hand
ssuccessor :: SPeano pn -> (SPeano (Successor pn))
ssuccessor pred =
case pred of
SZero -> SSuccessor pred
SSuccessor _ -> SSuccessor pred
lengthSPeano :: Vector pn st -> SPeano pn
lengthSPeano Nil = SZero
lengthSPeano (_ :+ xs) = ssuccessor (lengthSPeano xs)