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

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]
  }

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

EDIT 受@chi's answer的启发，我对第一个问题的解决方案是按以下方式使用类型族，因为实际上有很多游标种类和列举所有这些似乎是错误的：

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

如果你只关心防止构造，你可以使用

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 库自动生成。）

第二个问题，用一个existential和一个singleton:

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

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

Answer 2

另一种选择是使用 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)

我添加了 Show 实例以进行简单测试。现在您可能想知道 TestLit k 从何而来，这是它的定义，使用 Eval 和 Pure 来自 first-class-families 和 ConstraintKinds:

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 包。

现在第二个问题：

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

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

我们将只导出函数 getLiteralValue，而不导出类型 class 本身，因为我们要提供所有实例。对于这些，我们需要 FlexibleInstances 和 UndecidableInstances，以及 OVERLAPPING 和 OVERLAPPABLE pragmas。

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

如果您愿意，可以使类型 class 更复杂（使用额外参数）。如果愿意，您也可以从构造函数中删除 SCursorKind k（但我认为它提供了更好的 Show 实例）

Here's a runnable example online, using the defintions from Fcf inlined, and Data.Type.Equality since those seem to cause trouble on that site

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

Expressing dependencies between values of a record in types

haskell

dependent-type