0

我正在尝试对一个类型级别的图进行编码，该图对边的构造有一些限制（通过类型类），但是当我尝试为构造图取别名时遇到了“类型中的非法约束”错误。是什么导致了这个问题？如果它不可行，是否有另一种方法来编码图形结构，以便它可以按类型构建并折叠以产生图形的值级表示？

编辑：渴望

我希望能够将图形的构造限制在任何两个操作的input和output节点上。

为了清楚起见，让我们以众所周知的长度索引向量为例。

Anoperation将采用input某种形状，并可能将其长度更改为output. 两者之间的优势operations需要确保第一个的输出与第二个的输入兼容——对于某些实例定义的兼容性概念来说。（下面，这些约束被省略了；应用程序需要在编译时对约束进行依赖类型验证和类型计算。）

为了定义一个S可以与现有操作（T等）一起使用的新操作，只需添加数据类型S、实现S _ 和必要的约束S作为实例的功能类型类的Edge。

--Pragmas are needed additionally for the project in which this snippet is included
{-# LANGUAGE TypeInType, DataKinds, PolyKinds, ScopedTypeVariables,
  FlexibleInstances, FlexibleContexts, GADTs, TypeFamilies,
  RankNTypes, LambdaCase, TypeOperators, TemplateHaskell,
  ConstraintKinds, PolyKinds, NoImplicitPrelude,
  UndecidableInstances, MultiParamTypeClasses, GADTSyntax,
  AllowAmbiguousTypes, InstanceSigs, DeriveFunctor,
  FunctionalDependencies #-}

-- Algebra.Graph is from the algebraic-graphs package
import qualified Algebra.Graph as AG
import Data.Singletons
import Data.Singletons.Prelude
import Data.Singletons.TypeLits
import Data.Kind


data T (ln::Nat) c = T c

class Edge operation n o 

instance 
  -- This would be something like: (LengthIsValidPrime x ~ True, y ~ DependentlyTypedCalculationForOpabc x) => 
  Edge (T l c) x y

data Flow :: * -> * where
        Empty :: Flow (a)
        Vertex :: (Edge a n o) => a -> Flow (a)
        Connect ::
            (Edge a x y, Edge a y z, Edge a x z) =>
            Flow (a) -> Flow (a) -> Flow (a)
        Overlay ::
            (Edge a x y, Edge a y z, Edge a x z) =>
            Flow (a) -> Flow (a) -> Flow (a)



type Test c = Connect (Vertex (T 24 c )) (Vertex (T 3 c))
--which fails with

--error:
--    • Illegal constraint in a type: Edge a0 x0 z0
--    • In the type ‘Connect (Vertex (T  24 c)) (Vertex (T 3 c))’
--      In the type declaration for ‘Test’

-- We want to be able to define a graph like so: 
type InputNode c = Vertex (T 100 c )
type ForkNode c = Vertex (T 10 c )
type NodeB c = Vertex (T 1  c )
type NodeC c = Vertex (T 1  c )
type PathA c = Connect (InputNode c) (ForkNode c)
type PathAB c = Connect (PathA c) (NodeB c)
type PathAC c = Connect (PathA c) (NodeC c)
type Output c = Vertex (T 2 c )
type Subgraph c = Overlay (Connect (PathAC c) (Output c)) (Connect (PathAB c) (Output c))

-- and eventually the trascription from the type-level graph to a value graph defined by Algebra.Graph
--foldFlow :: Flow a -> AG.Graph (Flow a)
--foldFlow Empty         = AG.empty
--foldFlow vt@(Vertex x) = AG.vertex vt
--foldFlow (Overlay x y) = AG.overlay  (foldFlow x) (foldFlow y)
--foldFlow (Connect x y) = AG.connect  (foldFlow x) (foldFlow y)
--runGraph :: Subgraph c
--runGraph = ...create a term-level Subgraph c so we can fold over it.

要点在这里

4

0 回答 0