Проблемы с 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 [email protected](ZeroF      _) = Iterated singleton (getIterateF xs)
toIterated [email protected](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)
Другие вопросы по тегам