创建有效构造函数的列表

Cli*_*ton 8 haskell gadt

考虑以下:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}

data T = T1 | T2

data D (t :: T) where
  D1 :: D T1
  D2 :: D T2
  D3 :: D d
  D4 :: D T1

x1 :: [D T1]
x1 = [D1, D3, D4]

x2 :: [D T2]
x2 = [D2, D3]
Run Code Online (Sandbox Code Playgroud)

基本上x1是所有有效构造函数的列表D T1,并且x2是所有有效构造函数的列表D T2.

但是,我希望这两个列表能够反映添加的任何其他构造函数D,我不想像现在这样对这些列表进行硬编码.

有没有办法定义x1x2自动生成它们D

eps*_*lbe 2

免责声明 - 我的 TemplateHaskell-fu 几乎不存在 - 但我已经调查了一些,这应该为您提供一个使用的起点:

\n\n

对于那些不知道 Template Haskell 是一种元编程(语言)的人来说,它允许编写在编译时运行的程序 - 它经过类型检查,因此它是安全的(对于安全的某些定义,我认为你可以写需要无限时间编译的程序)。

\n\n
{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE KindSignatures #-}\n{-# LANGUAGE GADTs #-}\n{-# LANGUAGE TemplateHaskell #-}\n\nimport Language.Haskell.TH\n\ndata T = T1 | T2\n\ndata D (t :: T) where\n  D1 :: D T1\n  D2 :: D T2\n  D3 :: D d\n  D4 :: D T1\n
Run Code Online (Sandbox Code Playgroud)\n\n

您可以首先将文件加载到 GHCi 中(不要忘记:set -XTemplateHaskell那里)

\n\n
> typeInfo = reify ''D\n> $(stringE . show =<< typeInfo)\n
Run Code Online (Sandbox Code Playgroud)\n\n

typeInfo是一个Q Info允许您从类型中提取信息(由 转义'') -$(..)类似于 print 的工作方式。

\n\n

这将为您提供构建 (G)ADT 的模板 haskell 表达式:

\n\n
TyConI (\n    DataD [] TMP.D [KindedTV t_6989586621679027167 (ConT TMP.T)] Nothing \n        [GadtC [TMP.D1] [] (AppT (ConT TMP.D) (ConT TMP.T1))\n        ,GadtC [TMP.D2] [] (AppT (ConT TMP.D) (ConT TMP.T2))\n        ,ForallC [KindedTV d_6989586621679027168 (ConT TMP.T)] [] (GadtC [TMP.D3] [] (AppT (ConT TMP.D) (VarT d_6989586621679027168)))\n        ,GadtC [TMP.D4] [] (AppT (ConT TMP.D) (ConT TMP.T1))] [])\n
Run Code Online (Sandbox Code Playgroud)\n\n

我进行了一些模式匹配 - 您可以找到没有限制 ( ForallC) 或特定类型 ( TMP.T1/ TMP.T2) 的构造函数,然后编写一些表达式 - 从这些表达式创建一个新类型。

\n\n

现在我没有足够的时间来提供这一点 - 但我今晚会更新这个答案。

\n\n

编辑

\n\n

我更多地研究了构造类型,但我不得不承认我自己有点陷入困境 - 我成功地解构了类型信息。

\n\n
d = reify ''D\n\ndataName :: Info -> Maybe [Name]\ndataName (TyConI (DataD _ _ _ _ x _) )= Just [t | NormalC t _ <- x]\ndataName _ = Nothing\n\ngadtDataUnsafe :: Info -> Q Exp\ngadtDataUnsafe (TyConI (DataD _ _ _ _ cons _)) = return $ head $ concat [t | GadtC t _ _ <- cons]\n
Run Code Online (Sandbox Code Playgroud)\n\n

我认为从这里过滤T1//是可行的,虽然很乏味T2forall d但构建列表是可行的。

\n\n

我失败的是构造类型 - 如果我将文件加载到 ghci 我可以执行

\n\n
> f = $(gadtDataUnsafe =<< d)\n>:t f\nf :: D 'T1\n
Run Code Online (Sandbox Code Playgroud)\n\n

但如果我在文件中调用它,我会收到以下错误

\n\n
error:\n    \xe2\x80\xa2 GHC stage restriction:\n        \xe2\x80\x98gadtData\xe2\x80\x99 is used in a top-level splice, quasi-quote, or annotation,\n        and must be imported, not defined locally\n    \xe2\x80\xa2 In the untyped splice: $(gadtData =<< d)\n
Run Code Online (Sandbox Code Playgroud)\n\n

我知道,例如,Edward Kmett 制作了一些 th-magic 的东西,它在同一个文件中工作,但拼接没有分配给变量 - 所以也许你需要在 - I 中构建列表的Q Exp名称我猜mkName那里会有你需要的东西。

\n\n

这总结了我发现的所有内容 - 我希望它有帮助,我至少学到了一些东西 - 对于完整的答案,也许更聪明/对模板 haskell 更有经验的人可以在第二个答案中提供他/她的一些知识。

\n