haskell - 为什么此 GADT 上的模式匹配似乎会在类型检查器中引入歧义？

Question

我正在尝试实现 Abstract Syntax Graphs, as described by Andres Loeh and Bruno C. d. S. Oliveira 的形式.在大多数情况下，我似乎理解正确。但是，当我尝试将 letrec 引入我的语法时，我遇到了一些问题。我认为通过这个小代码示例更容易:

首先，一个小前奏:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
import Control.Applicative

infixr 8 :::
data TList :: (k -> *) -> [k] -> * where
  TNil :: TList f '[]
  (:::) :: f t -> TList f ts -> TList f (t ': ts)

tmap :: (forall a. f a -> g a) -> TList f as -> TList g as
tmap f (TNil) = TNil
tmap f (x ::: xs) = f x ::: tmap f xs

ttraverse :: Applicative i => (forall a. f a -> i (g a)) -> TList f xs -> i (TList g xs)
ttraverse f TNil = pure TNil
ttraverse f (x ::: xs) = (:::) <$> f x <*> ttraverse f xs

现在我可以定义我的语言的语法了。在这种情况下，我试图在我的视频游戏中描述二维级别。我有顶点(平面中的点)和墙壁(顶点之间的线段)。

data WallId
data VertexId

data LevelExpr :: (* -> *) -> * -> * where
  Let
    :: (TList f ts -> TList (LevelExpr f) ts)
    -> (TList f ts -> LevelExpr f t)
    -> LevelExpr f t

  Var :: f t -> LevelExpr f t

  Vertex :: (Float, Float) -> LevelExpr f VertexId

  Wall
    :: LevelExpr f VertexId
    -> LevelExpr f VertexId
    -> LevelExpr f WallId

在 PHOAS 之后，我们使用更高等级的类型来对 f 的选择强制执行参数化。 :

newtype Level t = Level (forall f. LevelExpr f t)

最后，让我们为 letrec 介绍一些语法糖。自动用 Var 标记所有内容，正如论文所建议的:

letrec :: (TList (LevelExpr f) ts -> TList (LevelExpr f) ts)
       -> (TList (LevelExpr f) ts -> LevelExpr f t)
       -> LevelExpr f t
letrec es e =
  Let (\xs -> es (tmap Var xs))
      (\xs -> e (tmap Var xs))

我们现在可以用这种语言编写一些程序。这是一个简单的表达式，它引入了两个顶点并在它们之间定义了一堵墙。

testExpr :: Level WallId
testExpr =
  Level (letrec (\ts ->
                   Vertex (0,0) :::
                   Vertex (10,10) :::
                   TNil)
                (\(v1 ::: v2 ::: _) ->
                   Wall v1 v2))

这工作得很好。一个等价的表达式是使用 letrec 定义两个顶点和它们之间的墙，全部绑定(bind)。在 letrec 的主体中，我们可以只返回墙绑定(bind)。我们首先将墙移动到 letrec 中，然后添加一些洞来看看 GHC 知道什么:

testExprLetrec :: Level WallId
testExprLetrec =
  Level (letrec (\ts ->
                   Vertex (0,0) :::
                   Vertex (10,10) :::
                   Wall _ _ :::
                   TNil)
                _)

GHC 通知我们:

y-u-no-infer.hs:74:25:
    Found hole `_' with type: LevelExpr f VertexId
    Where: `f' is a rigid type variable bound by
               a type expected by the context: LevelExpr f WallId
               at y-u-no-infer.hs:71:3
    Relevant bindings include
      ts :: TList (LevelExpr f) '[VertexId, VertexId, WallId]
        (bound at y-u-no-infer.hs:71:19)
      testExprLetrec :: Level WallId (bound at y-u-no-infer.hs:70:1)
    In the first argument of `Wall', namely `_'
    In the first argument of `(:::)', namely `Wall _ _'
    In the second argument of `(:::)', namely `Wall _ _ ::: TNil'

好的，很好 - GHC 知道 ts包含两个 VertexId s 和 WallId .我们
应该能够在 ts 上进行模式匹配提取这些表达式中的每一个。

testExprLetrec2 :: Level WallId
testExprLetrec2 =
  Level (letrec (\ts@(v1 ::: v2 ::: _) ->
                   Vertex (0,0) :::
                   Vertex (10,10) :::
                   Wall v1 v2 :::
                   TNil)
                _)

当我尝试输入检查时，我会看到

y-u-no-infer.hs:109:20:
    Could not deduce (t ~ VertexId)
    from the context (ts0 ~ (t : ts))
      bound by a pattern with constructor
                 ::: :: forall (k :: BOX) (f :: k -> *) (t :: k) (ts :: [k]).
                        f t -> TList f ts -> TList f (t : ts),
               in a lambda abstraction
      at y-u-no-infer.hs:108:23-37
    or from (ts ~ (t1 : ts1))
      bound by a pattern with constructor
                 ::: :: forall (k :: BOX) (f :: k -> *) (t :: k) (ts :: [k]).
                        f t -> TList f ts -> TList f (t : ts),
               in a lambda abstraction
      at y-u-no-infer.hs:108:23-31
      `t' is a rigid type variable bound by
          a pattern with constructor
            ::: :: forall (k :: BOX) (f :: k -> *) (t :: k) (ts :: [k]).
                   f t -> TList f ts -> TList f (t : ts),
          in a lambda abstraction
          at y-u-no-infer.hs:108:23
    Expected type: TList (LevelExpr f) ts0
      Actual type: TList (LevelExpr f) '[VertexId, VertexId, WallId]
    Relevant bindings include
      v1 :: LevelExpr f t (bound at y-u-no-infer.hs:108:23)
    In the expression:
      Vertex (0, 0) ::: Vertex (10, 10) ::: Wall v1 v2 ::: TNil
    In the first argument of `letrec', namely
      `(\ ts@(v1 ::: v2 ::: _)
          -> Vertex (0, 0) ::: Vertex (10, 10) ::: Wall v1 v2 ::: TNil)'
    In the first argument of `Level', namely
      `(letrec
          (\ ts@(v1 ::: v2 ::: _)
             -> Vertex (0, 0) ::: Vertex (10, 10) ::: Wall v1 v2 ::: TNil)
          _)'

为什么 GHC 现在期待 TList (LevelExpr f) ts0 , 当它以前是新的 ts0 ~ '[VertexId, VertexId, WallId] ?

Answer 1

类型推断不能可靠地与 GADT 一起使用。您可以通过提供简单的类型注释来修复代码:

testExprLetrec2 :: Level WallId
testExprLetrec2 =
  Level (letrec ((\ts@(v1 ::: v2 ::: _
                       :: TList (LevelExpr f) '[VertexId, VertexId, WallId]) ->
                   Vertex (0,0) :::
                   Vertex (10,10) :::
                   Wall _ _ :::
                   TNil)
                   )
                _)