1

语境

我正在尝试实现一个与 IBM 的 OLP(线性编程建模语言)松散相似的 EDSL。

代码

Haskell EDSL 代码

{-# 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]]
[[[Double]]]
...
4

2 回答 2

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一些kIterate 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,您不需要做任何额外的工作来访问索引的实际值 - 只需在向量上进行模式匹配。

于 2016-04-24T15:13:39.297 回答
0

您有几个选择,所有这些都相当于在值级别对迭代深度进行编码,以便您可以对其进行模式匹配。

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 为我处理的证明,所以我将保留IterateF GADT周围并根据它编写函数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列表。您可以将它用于简单的情况,例如showing 嵌套值,或者您可以将 转换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)
于 2016-04-24T01:19:36.530 回答