表示有效类型的 Haskell 数据类型

Posted 2023-03-28

【中文标题】表示有效类型的 Haskell 数据类型

【英文标题】：Haskell data type that represents valid types

【发布时间】：2017-03-03 01:34:19

【问题描述】：

是否有一个库定义了定义有效 Haskell 类型的数据类型（可能是 GADT）。

为了解释，让我建议这可能是什么样子：

data A
data B

class Free t
instance Free A
instance Free B

x = Forall A (Forall B (Constraint (NumConstraint A) 
      (Constructor Function A (Constructor Function B A))))

这将表示：

forall a b. Num a => a -> b -> a

我并不是说我所建议的是一个好的实现，我只是想表明我的意思。

当然，如果您可以定义类型定义的语法，您就可以创建一个 GADT 来表示它。有什么已经这样做了吗？

【问题讨论】：

为什么是 GADT 而不是 ADT？ template-haskell 是你要找的吗？

我不介意它是否是 GADT，只要我能做到漂亮打印它们等。

【参考方案1】：

您正在寻找the type-related ADTs in template-haskell。请注意Type 是Ppr 的一个实例，它具有ppr 漂亮打印功能。

ghci> import Language.Haskell.TH
ghci> :
ghci> x <- runQ $ do
ghci|        a <- newName "a"
ghci|        b <- newName "b"
ghci|        pure $ ForallT [PlainTV a,PlainTV b] [AppT (ConT (mkName "Num")) (VarT a)] (AppT (AppT ArrowT (VarT a)) (AppT (AppT ArrowT (VarT b)) (VarT a)))
ghci| :
ghci> x
ForallT [PlainTV a_4,PlainTV b_5] [AppT (ConT Num) (VarT a_4)] (AppT (AppT ArrowT (VarT a_4)) (AppT (AppT ArrowT (VarT b_5)) (VarT a_4)))
ghci> ppr x
forall a_0 b_1 . Num a_0 => a_0 -> b_1 -> a_0

事实上，GHC 的TemplateHaskell 语言扩展将使玩这个游戏变得非常容易。不必写出ForallT ... 的东西，我可以“引用”我正在寻找的类型

ghci> :set -XTemplateHaskell -XExplicitForall
ghci> x' <- runQ [t| forall a b. Num a => a -> b -> a |]

而x' 与x 相同（也许a 和b 最终会略有不同Names，但仍然如此）！