表示类型中记录值之间的依赖关系

Question

假设我们试图表示类C语言的AST节点。首先，为简单起见，让我们定义节点类型的概念：

data CursorKind = KIntegerLiteral | KStringLiteral | KFunction | KStruct | KTypedef

接下来，让我们添加一个类型，以类型安全的方式表示文本的值：

data LiteralValue k where
IntegerValue :: Int -> LiteralValue 'KIntegerLiteral
StringValue :: String -> LiteralValue 'KStringLiteral
NotALiteral :: LiteralValue '???

这是第一个问题：有没有办法定义NotALiteral子句，以便它暗示除KIntegerLiteral和KStringLiteral之外的任何k？如果不是，表达这种后备条款以避免重复的最佳方式是什么？

无论如何，现在，鉴于上述内容，让我们在 AST 中构造一个非常简单的节点表示：

data Cursor = Cursor
{ kind :: CursorKind
, value :: LiteralValue ???
, children :: [Cursor]
}

这是第二个问题。理想情况下，我想要的是依赖于kind的value类型。在像Idris这样具有完全依赖类型的语言中，它会非常简单。但是我们如何在现代Haskell中做到这一点，它必须提供所有单例和TypeInType？

---

编辑受@chi的回答的启发，我对第一个问题的解决方案是按以下方式使用类型族，因为实际上有大量的游标类型，枚举所有这些似乎都是错误的：

type family NotALiteral (k :: CursorKind) :: Bool where
NotALiteral 'KIntegerLiteral = 'False
NotALiteral 'KStringLiteral = 'False
NotALiteral a = 'True
data LiteralValue k where
IntegerValue :: Int -> LiteralValue 'KIntegerLiteral
StringValue :: String -> LiteralValue 'KStringLiteral
NotALiteral :: NotALiteral k ~ 'True => LiteralValue k

现在的问题在于一个函数的实现，该函数在给定游标类型k的情况下生成匹配LiteralValue。理想情况下，我们希望具有以下签名的内容(是的，我正在使用singletons(：

getLiteralValue :: Sing k -> FFICursor -> FFIMonad (LiteralValue k)

对于k确实是文字的情况，实现非常简单：

getLiteralValue SKIntegerLiteral ffi = IntegerValue <$> ffiGetInt ffi
getLiteralValue SKStringLiteral ffi = StringValue <$> ffiGetStr ffi

但是如果我们现在尝试写类似的东西

getLiteralValue _ _ = pure NotALiteral

它不会进行类型检查，因为 GHC 无法得出NotALiteral k ~ 'True成立。一种解决方案是继续在单例上匹配，但它实际上需要枚举所有类型，由于它们的数量，我想再次避免这种情况。有没有更好的方法？

Answer 1

另一种选择是使用first-class-families包创建自定义 TypeError，并对约束进行自定义检查。

从语言扩展开始：

{-# LANGUAGE
GADTs,
StandaloneDeriving,
ConstraintKinds,
DataKinds,
TypeFamilies,
TypeInType,
TypeOperators,
ExplicitNamespaces,
FlexibleInstances,
UndecidableInstances 
#-}

接下来，导入

import Data.Kind (Constraint)
import Data.Type.Equality (type (==))
import Data.Type.Bool (If, type (||))
import GHC.TypeLits (TypeError, ErrorMessage(..))
-- package: first-class-families
import Fcf (Eval, Exp, Pure)

接下来，我们需要定义一个数据类型来延迟类型错误，因此除非必要，否则不会对其进行计算。还要为Eval定义一个类型实例

data TypeError' :: ErrorMessage -> Exp a
type instance Eval (TypeError' m) = TypeError m

现在我们将要使用的类型

data CursorKind = KIntegerLiteral | KStringLiteral | KFunction | KStruct | KTypedef 
-- Singletons for pattern matching on NotALiteral, can be generated with the singletons package
data SCursorKind (k :: CursorKind) where
SKIntegerLiteral :: SCursorKind 'KIntegerLiteral
SKStringLiteral :: SCursorKind 'KStringLiteral
SKFunction :: SCursorKind 'KFunction
SKStruct :: SCursorKind 'KStruct 
SKTypedef :: SCursorKind 'KTypedef
deriving instance Show (SCursorKind k)
data LiteralValue (k :: CursorKind) where
IntegerValue :: Int -> LiteralValue 'KIntegerLiteral
StringValue :: String -> LiteralValue 'KStringLiteral
NotALiteral :: TestLit k => SCursorKind k -> LiteralValue k
deriving instance Show (LiteralValue k)

我添加了用于简单测试的显示实例。现在你可能想知道TestLit k来自哪里，这是它的定义，使用first-class-families和ConstraintKinds的Eval和Pure：

type TestLit k = Eval (
If (k == 'KIntegerLiteral || k == 'KStringLiteral)
(TypeError' ('Text "Wrong CursorKind, shouldn't be KIntegerLiteral or KStringLiteral, but got: " :<>: 'ShowType k)) 
-- ^could probably give a better TypeError
(Pure EmptyConstrant)
)
-- because (Pure (() :: Constraint)) has way too many parentheses
type EmptyConstrant = (() :: Constraint)

在这一点上，我们和 chi 得到我们处于同一点，即当我们尝试编译表达式NotALiteral SKIntegerLiteral时，我们得到一个类型错误(也适用于字符串文字(。 您还可以对约束使用简单的类型族(使用自定义 TypeError(，而不是使用first-class-families包。

现在来看第二个问题：

要实现您想要的，您可以使用类型类。我将稍微简化这个问题。假设我们想要一个函数SCursorKind k -> LiteralValue k，并且我们希望将其专门用于文字，并将其默认为其他文字，而不必指定所有函数。我们将定义一个类型类：

class LitVal k where
getLiteralValue :: SCursorKind k -> LiteralValue k

我们只会导出函数getLiteralValue，而不是类型类本身，因为我们希望提供所有实例。我们需要 FlexibleInstances 和 UndecidableInstances，以及 OVERLAPPING 和 OVERLAPPABLE 编译指示。

instance {-# OVERLAPPING #-} LitVal 'KIntegerLiteral where
getLiteralValue _ = IntegerValue 4
instance {-# OVERLAPPING #-} LitVal 'KStringLiteral where
getLiteralValue _ = StringValue "4"
instance {-# OVERLAPPABLE #-} TestLit k => LitVal k where
getLiteralValue sk = NotALiteral sk

如果您愿意，可以使类型类更复杂(带有额外的参数(。如果您愿意，您也可以从构造函数中删除SCursorKind k(但在我看来，它提供了一个更好的Show实例(

这是一个在线运行的可运行示例，使用来自 Fcf 内联和 Data.Type.Equality 的定义，因为这些定义似乎在该站点上造成麻烦

Answer 2

如果你只关心防止施工，你可以使用

data LiteralValue k where
...
NotALiteral :: NonLiteral k => LiteralValue k
class NonLiteral k
instance NonLiteral 'KFunction
...

请注意，在这种方法中，k的值会在运行时之前被擦除，因此我们将无法对此进行模式匹配。 如果知道k很重要，那么我们可以使用单例

data SCursorKind c where
SKIntegerLiteral :: SCursorKind 'KIntegerLiteral
SKStringLiteral  :: ScursorKind 'KStringLiteral
...
data LiteralValue k where
...
NotALiteral :: NonLiteral k => SCursorKind k -> LiteralValue k

这样我们就有一些模式匹配的东西。

(我认为单例类型也可以使用singletons库自动生成。

对于第二个问题，使用存在和单例：

data Cursor where
Cursor ::
{ kind :: SCursorKind k
, value :: LiteralValue k
, children :: [Cursor]
} -> Cursor

这会稍微更改字段的类型kind。如果这是一个问题，那么编写一个fromSCursorKind :: SCursorKind k -> CursorKind函数来恢复原始类型是微不足道的。