Моделирование гетерогенных графов в Хаскеле - PullRequest
Новая
       26

Моделирование гетерогенных графов в Хаскеле

0 голосов
/ 28 апреля 2018

Как я могу смоделировать то, что я буду называть «гетерогенными графами» в haskell, чтобы корректность типов графа можно было проверить во время компиляции?

Для этой цели гетерогенный граф представляет собой набор узлов, каждый с определенной меткой типа, и набор ребер, каждый с меткой типа источника и меткой типа назначения.

Мы хотим статически обеспечить, чтобы при добавлении ребра к графику метка типа источника этого ребра соответствовала метке типа узла источника, а метка типа назначения этого ребра соответствовала метка типа узла назначения. Но мы не хотим делать это тривиальным способом (заставляя весь граф содержать только узлы с одной конкретной меткой типа).

1 Ответ

0 голосов
/ 28 апреля 2018

Я не уверен, как бы я применил это во время компиляции - я думаю, что это требует, чтобы ваши графики были полностью статичными? - но это довольно просто применить во время выполнения, используя Typeable. Вот эскиз того, как это будет выглядеть. Сначала я начну с напечатанных типов Node и Edge: 

data Node a = Node a
data Edge a b = Edge !Int !Int

Оберните их в экзисте: 

{-# LANGUAGE ExistentialQuantification #-}

import Data.Typeable

data SomeNode
  = forall a. (Typeable a)
  => SomeNode (Node a)

data SomeEdge
  = forall a b. (Typeable a, Typeable b)
  => SomeEdge (Edge a b)

Иметь тип данных разнородного графа, который использует экзистенциально количественные типы: 

import Data.IntMap (IntMap)

-- Not a great representation, but simple for illustration.
data Graph = Graph !(IntMap SomeNode) [SomeEdge]

А затем операции, выполняющие динамические проверки типов: 

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

import qualified Data.IntMap as IntMap

addNode
  :: forall a. (Typeable a)
  => Int -> a -> Graph -> Maybe Graph
addNode i x (Graph ns es) = case IntMap.lookup i ns of

  -- If a node already exists at a given index:
  Just (SomeNode (existing :: Node e)) -> case eqT @e @a of

    -- Type-preserving replacement is allowed, but…
    Just Refl -> Just $ Graph ns' es

    -- …*type-changing* replacement is *not* allowed,
    -- since it could invalidate existing edges.
    Nothing -> Nothing

  -- Insertion is of course allowed.
  Nothing -> Just $ Graph ns' es

  where
    ns' = IntMap.insert i (SomeNode (Node x)) ns

-- To add an edge:
addEdge
  :: forall a b. (Typeable a, Typeable b)
  => Edge a b -> Graph -> Maybe Graph
addEdge e@(Edge f t) (Graph ns es) = do

  -- The ‘from’ node must exist…
  SomeNode (fn :: Node tfn) <- IntMap.lookup f ns
  -- …and have the correct type; and
  Refl <- eqT @a @tfn

  -- The ‘to’ node must exist…
  SomeNode (tn :: Node ttn) <- IntMap.lookup t ns
  -- …and have the correct type.
  Refl <- eqT @b @ttn

  pure $ Graph ns $ SomeEdge e : es

Теперь это удается: 

pure (Graph mempty mempty)
  >>= addNode 0 (1 :: Int)
  >>= addNode 1 ('x' :: Char)
  >>= addEdge (Edge 0 1 :: Edge Int Char)

Но изменение Int / Char в Edge Int Char на недопустимые типы или 0 / 1 на недопустимые индексы приведет к ошибке и вернет Nothing.

...