haskell - 将 GADT 与 DataKinds 用于函数中的类型级数据构造函数约束

Question

我正在尝试将 GADT 与 DataKinds 一起使用，如下所示

{-# LANGUAGE KindSignatures, DataKinds, GADTs #-}
module NewGadt where

data ExprType = Var | Nest

data Expr (a :: ExprType) where
  ExprVar :: String -> Expr Var
  ExprNest :: Expr a -> Expr Nest

data BaseExpr
  = BaseExprVar String
  | BaseExprNest BaseExpr

translate :: BaseExpr -> Expr a
translate (BaseExprVar id) = ExprVar id
translate (BaseExprNest expr) = ExprNest $ translate expr

编译错误:

/home/elijah/code/monty/src/NewGadt.hs:15:32: error:
    • Couldn't match type ‘a’ with ‘'Var’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          bexprToExpr :: forall (a :: ExprType). BaseExpr -> Expr a
        at src/NewGadt.hs:14:1-33
      Expected type: Expr a
        Actual type: Expr 'Var
    • In the expression: ExprVar id
      In an equation for ‘bexprToExpr’:
          bexprToExpr (BaseExprVar id) = ExprVar id
    • Relevant bindings include
        bexprToExpr :: BaseExpr -> Expr a (bound at src/NewGadt.hs:15:1)
   |
15 | bexprToExpr (BaseExprVar id) = ExprVar id
   |                                ^^^^^^^^^^

我想这样做，所以某些函数只能在特定类型的 expr 上工作，例如:

printVariable :: Expr Var -> IO ()
printVariable (ExprVar id) = putStrLn id

printNested :: Expr Nest -> IO ()
printNested (ExprNest inner) = putStrLn "nested expression"

printExpr :: Expr a -> IO ()
printExpr expr@ExprVar {} = printVariable expr
printExpr expr@ExprNest {} = printNested expr

当然，拨打 printVariable与 Expr Nest应该编译失败。
有没有办法让翻译函数返回 Expr a像这样？或者这是对 DataKinds 和 GADT 的不当使用？
编辑:
解决方案有效!但是，我必须升级到 ghc >=8.10 并启用 StandaloneKindSignatures, PolyKinds

Answer 1

你可以定义一个存在的包装器

{-# Language PolyKinds                #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications         #-}

import Data.Kind (Type)

--
--   Exists @ExprType :: (ExprType -> Type) -> Type
--
type Exists :: forall k. (k -> Type) -> Type
data Exists f where
  Exists :: f x -> Exists f

并返回 Exists Expr

translate :: BaseExpr -> Exists @ExprType Expr
translate (BaseExprVar id)
  = Exists (ExprVar id)
translate (BaseExprNest expr)
  | Exists a <- translate expr
  = Exists (ExprNest a)

这使用 pattern guards解压存在类型

pattern guards are of the form p <- e, where p is a pattern (see Section 3.17) of type t and e is an expression type t1. They succeed if the expression e matches the pattern p, and introduce the bindings of the pattern to the environment.

Haskell Report

并且等价于这些

translate (BaseExprNest expr) = case translate expr of
  Exists a -> Exists (ExprNest a)

{-# Language ViewPatterns #-}

translate (BaseExprNest (translate -> Expr a)) = Exists (ExprNest a)

但是试试 let或 where它不会工作。
引用

Stitch: The Sound Type-Indexed Type Checker

An Existential Crisis Resolved