haskell - 评估每个节点具有任意数量依赖项的强类型计算图

Question

我想评估一个简单的计算图。我能够为计算图编写代码来执行此操作，其中每个非终端节点都有两个依赖项(这可以简单地扩展到任何固定数量的依赖项)

{-# LANGUAGE ExistentialQuantification #-}

module Graph where

-- Have:
data Node a =
    forall u v . CalculationNode { f :: u -> v -> a
                                 , dependencies :: (Node u, Node v) }
  | TerminalNode { value :: a }

eval :: Node a -> a
eval (CalculationNode f (d1, d2)) = f (eval d1) (eval d2)
eval (TerminalNode v) = v

three :: Node Int
three = TerminalNode 3

abcd :: Node String
abcd = TerminalNode "abcd"

seven :: Node Int
seven = CalculationNode (\ s i -> i + length s) (abcd, three)

问题是:我如何扩展这段代码，以便笔记可以接受任意数量的依赖项？

类似于:

data Node a =
    forall u_1 u_2 ... u_n . CalculationNode { f :: u_1 -> u_2 -> ... -> u_n -> a
                                             , dependencies :: (Node u_1, Node u_2, ... , Node u_n) }
  | TerminalNode { value :: a }

eval :: Node a -> a
eval = ?

我怀疑这需要一些 typefamily/hlist 魔法，但我什至不知道从哪里开始。欢迎解决方案和提示。

Answer 1

当然，有了一点“魔法”，这可以很好地概括:

{-# LANGUAGE PolyKinds, ExistentialQuantification, DataKinds, TypeOperators, TypeFamilies, GADTs #-} 

import Data.Functor.Identity 

type family (xs :: [*]) :-> (r :: *) :: * where 
  '[] :-> r = r 
  (x ': xs) :-> r = x -> (xs :-> r) 

此类型族表示 n 元函数。我认为这个定义很明显。

infixr 5 :>
data Prod (f :: k -> *) (xs :: [k]) where 
  Nil :: Prod f '[] 
  (:>) :: f x -> Prod f xs -> Prod f (x ': xs) 

此数据类型是一个索引类型列表的向量。这不太明显。您需要以某种方式在 Node 中存储类型变量列表 - 但每个类型变量都必须应用 Node。这个公式使它变得简单:

data Node a 
  = forall vs . CalculationNode (vs :-> a) (Prod Node vs)
  | TerminalNode a  

然后是一些辅助函数:

appFn :: vs :-> a -> Prod Identity vs -> a 
appFn z Nil = z 
appFn f (x :> xs) = appFn (f $ runIdentity x) xs 

mapProd :: (forall x . f x -> g x) -> Prod f xs -> Prod g xs 
mapProd _ Nil = Nil 
mapProd f (x :> xs) = f x :> mapProd f xs 

并且您的 eval 函数几乎和以前一样简单:

eval :: Node a -> a 
eval (TerminalNode a) = a 
eval (CalculationNode fs as) = appFn fs $ mapProd (Identity . eval) as

关于您的示例的唯一改变是用 Prod 构造函数替换元组:

seven = CalculationNode (\s i -> i + length s) (abcd :> three :> Nil)