行类型级别列表的多态相等

TL;DR: 我想使用 type family RIso (a :: [*]) (b :: [*]) :: Bool 实现行多态的统一，但是已经卡住了 .

背景

我正在为一种具有效果系统的语言编写一个编译器，该系统使用行多态，如Extensible Records with Scoped Labels，表示附加到函数类型的效果集 . 也就是说，在这种语言中，函数箭头的类型是：

(->) :: * -> * -> Effect -> *

其中 Effect 是一系列效果标签，例如 IO 或 Unsafe - 标签的“缺点”，具有另一个效果行，效果类型变量或“纯”效果（空行） . 一个简单的例子是 map 的类型：

<A, B, +E> (List<A>, (A -> B +E) -> List<B> +E)

在假设的Haskell语法中：

forall (a :: *) (b :: *) (e :: Effect).
  (a -> Eff e b) -> [a] -> Eff e [b]

这意味着 map 采用 A 类型的 List ，以及 A 到 B 的函数和一组效果 +E ，并返回 List 的 B ，也需要效果 +E . 纯函数的效果是完全多态的，默认为空行;所以 map 是纯粹的，如果它的功能论证是纯粹的;否则它需要与其参数相同的效果 .

我正在尝试在Haskell的类型系统中表示这种语言的类型系统，这样我就可以依靠Haskell的类型检查器以this blog post的方式编写经过验证的类型检查器 .

但是，当我开始统一函数类型时，我需要通过常规统一（相等）来统一输入和输出，但我需要通过行统一来统一效果，其定义如下：

s ≃ { l | s′ } : θ₁
tail(r) ∉ dom(θ₁)    -- †
θ₁(r) ~ θ₁(s′) : θ₂
---------------------------------------- [uni-row]
{ l | r } ~ s : θ₂ ∘ θ₁

这表示“如果 s 可以被替换为 { l | s′ } ，取代 θ₁ ， r 和 s′ 统一替换 θ₂ ，那么 { l | r } 与 s 统一替换 θ₂ ∘ θ₁ ，再加上标有匕首（†）的边条件我将立即解释 .

（≃）关系表示根据以下三个规则，两行是同构的：

-------------------------- [row-head]
{ l | r } ≃ { l | r } : []

l ≠ l′
r ≃ { l | r′ } : θ
-------------------------------- [row-swap]
{ l′ | r } ≃ { l | l′ | r′ } : θ

fresh(β)
----------------------------- [row-var]
α ≃ { l | β } : [α ↦ {l | β}]

在我目前未经验证的类型检查器中，这两个函数在Haskell中看起来像这样：

unify typeEnv0 (Row l r) s = do

  -- Attempt to rewrite.
  maybeSubstitution <- isomorphicRows typeEnv0 l s (rowLast r)
  case maybeSubstitution of

    -- If rows are isomorphic:
    Just (s', substitution, typeEnv1) -> case substitution of

      -- Apply substitution, if any, and unify the tails.
      Just (x, t) -> let
        typeEnv2 = typeEnv1
          { typeEnvVars = Map.insert x t $ typeEnvVars typeEnv1 }
        in unify typeEnv2 r s'
      Nothing -> unify typeEnv1 r s'

    -- Non-isomorphic rows do not unify.
    Nothing -> reportTypeMismatch (Row l r) s

-- Gets the last element in a row.
rowLast :: Type -> Type
rowLast (Row _ r) = rowLast r
rowLast t = t

isomorphicRows 实现了论文中描述的规则：

当一行{l | r}与某些行统一，我们首先尝试以{l |形式重写s s'} [...]如果这成功了，统一就会通过统一......行尾 .

因此，给定 l ， r 和 s ，以及统一规则， isomorphicRows 用于断言 s 可以在某些替换下被重写为 { l | r } ，失败（ Nothing ）或返回（ Just ）重写行的尾部，替换（ Maybe 因为它总是空的或单例），以及更新的类型环境 . 我们实际上并没有传递 r 因为我们只需要它的最后一个元素 rt .

isomorphicRows
  :: TypeEnv    -- Type environment
  -> Type       -- Effect label l
  -> Type       -- Effect row s
  -> Type       -- Effect row rt
  -> Typecheck
    (Maybe
      ( Type
      , Maybe (TypeId, Type)
      , TypeEnv
      ))

[row-head] 规则：已经以给定标签开头的行由身份替换轻易地重写 .

isomorphicRows typeEnv0 l (Row l' r') _rt
  | l == l'
  = pure $ Just (r', Nothing, typeEnv0)

[row-swap] 规则：在其中包含标签的行可以被重写以将该标签放在头部 .

isomorphicRows typeEnv0 l (Row l' r') rt
  | l /= l' = do
  maybeSubstitution <- isomorphicRows typeEnv0 l r' rt
  pure $ case maybeSubstitution of
    Just (r'', substitution, typeEnv1) -> Just
      (Row l r'', substitution, typeEnv1)
    Nothing -> Nothing

[row-var] 规则：当与类型变量统一时，不存在标签，因此我们不能直接测试相等性，并且必须为行尾返回一个新变量 .

†这会强制执行侧面条件，以防止统一具有共同尾部但具有不同前缀的行，从而确保即使我们添加新类型变量也会终止 .

isomorphicRows typeEnv0 l r@(TypeVar a) rt
  | r /= rt = do
  (b, typeEnv1) <- freshTypeVar typeEnv0
  pure $ Just (b, Just (a, Row l b), typeEnv1)

在任何其他情况下，行不是同构的 .

isomorphicRows _ _ _ _ = Nothing

我试过的

我正在尝试将行统一与 isomorphicRows 转换为类型级别，使用在类型级别类型列表上运行的类型族：

type family RIso (ra :: [*]) (rb :: [*]) :: Bool where

  -- [row-head]
  RIso ((l) ': r) ((l) ': s) = RIso r s

  -- [row-swap]
  RIso ((l) ': (l') ': r) ((l') ': (l) ': r)
    = TNot (TEq l l')

  RIso r r = 'True

  RIso _ _ = 'False

type family TNot (a :: Bool) :: Bool where
  TNot 'False = 'True
  TNot 'True = 'False

type family TEq (a :: Bool) (b :: Bool) :: Bool where
  TEq a a = 'True
  TEq _ _ = 'False

这似乎适用于基本情况：

> :kind! RIso '[] '[]
'True

> :kind! RIso '[Int] '[Int]
'True

> :kind! RIso '[Int, Char] '[Char, Int]
'True

> :kind! RIso '[Int, Char] '[Int, String]
'False

> :kind! RIso '[Int, Char, String] '[Char, Int, String]
'True

但在更复杂的情况下失败：

> :kind! RIso '[Int, String, Char] '[Char, Int, String]
'False

我相信这是因为我可能错误地实施了 [row-swap] 规则（ TNot 看起来很可疑），而且我错过了 [row-var] 规则 . 我坚持 [row-var] 的实现，因为我不知道如何将新的类型变量带入范围（或者这是否是正确的方法） . 我试过这个：

type family REq (ra :: [*]) (rb :: [*]) :: Bool where
  …
  -- [row-var]
  REq (l ': r) rt = TAnd (TNot (TEq r rt)) (TEq r (Row l b))
  …

type family TAnd (a :: Bool) (b :: Bool) :: Bool where
  TAnd 'True 'True = 'True
  TAnd _ _ = 'False

但是我发现免费的 b 会产生类型错误并不奇怪：

error: Not in scope: type variable ‘b’

问题

• 是否可以使用 forall 引入一个新变量，或者我应该放弃尝试直接实现输入规则并采取不同的方法？

• 或者，是否有一些现有的可扩展记录库专门使用行统一（而不是其他方法），所以我可以使用该库或从中学习技术？

请注意，这与简单的集合相等不同，因为可能存在重复的标签，并且它们是在我在本问题顶部链接的论文中描述的意义上的“范围” . 这有两个重要原因：首先，我打算将来扩展它，以便效果标签可以有类型参数，例如 ST s ;第二，我打算用这个机器来实现可扩展的记录和变体语言 .