如何在Idris 2中获取数据构造函数列表？是否有更优实现？

你的现有实现确实可以正常工作，但我们可以通过简化代码逻辑、提升复用性来优化它。以下是几种更优的方案：

方案1：简化现有实现的代码结构 #

你可以简化构造List的过程，不需要手动用foldr拼接，直接使用List的语法糖生成表达式，让代码更简洁易读：

module GetConstructors

import Language.Reflection

%language ElabReflection

data Color = Red | Green | Blue

Show Color where
  show Red = "Red"
  show Green = "Green"
  show Blue = "Blue"

colors : List Color
colors = %runElab do
  let tyName = NS (MkNS ["GetConstructors"]) (UN $ Basic "Color")
  conNames <- getCons tyName
  -- 直接生成 [Con1, Con2, ...] 形式的列表表达式
  let conExprs = map (\n => IVar EmptyFC n) conNames
  check $ `(the (List Color) [~(conExprs)])

main : IO () 
main = do
  putStrLn "Colors:"
  traverse_ (\c => putStrLn $ "  " ++ show c) colors

方案2：封装为可复用的通用宏 #

如果需要多次获取不同类型的构造函数列表，可以封装一个通用宏，避免重复编写相同逻辑：

module GetConstructors

import Language.Reflection

%language ElabReflection

-- 通用宏：自动解析目标列表的元素类型，返回其所有构造函数的列表
%macro
getConsList : Elab (List a)
getConsList = do
  (_, ty) <- getGoal
  case ty of
    App (TyCon listTy) elemTy => do
      let elemTyName = case elemTy of
                           TyCon name => name
                           _ => fail "仅支持获取代数数据类型的构造函数列表"
      conNames <- getCons elemTyName
      let conExprs = map (\n => IVar EmptyFC n) conNames
      check $ `(the (List ~(elemTy)) [~(conExprs)])
    _ => fail "目标类型必须是 List a"

data Color = Red | Green | Blue

Show Color where
  show Red = "Red"
  show Green = "Green"
  show Blue = "Blue"

-- 直接调用宏即可获取构造函数列表
colors : List Color
colors = getConsList

-- 示例：用于其他代数类型
data Shape = Circle Float | Square Float | Triangle Float Float
shapes : List Shape
shapes = getConsList

main : IO () 
main = do
  putStrLn "Colors:"
  traverse_ (\c => putStrLn $ "  " ++ show c) colors
  putStrLn "\nShapes:"
  traverse_ (\s => putStrLn $ "  " ++ show s) shapes

这个宏会自动识别目标列表的元素类型，无需手动指定类型的命名空间和名称，复用性极强。

方案3：基于Generic接口实现（适合复杂场景） #

如果你的类型已经实现了Generic接口，可以利用该接口的元数据来获取构造函数信息，适合需要对构造函数进行更复杂操作的场景：

module GetConstructors

import Language.Reflection
import Generics.Derive

%language ElabReflection
%language DeriveGeneric

data Color = Red | Green | Blue
%derive Generic Color

Show Color where
  show Red = "Red"
  show Green = "Green"
  show Blue = "Blue"

-- 基于Generic接口的通用宏
%macro
getConsListGeneric : Elab (List a)
getConsListGeneric = do
  (_, ty) <- getGoal
  case ty of
    App (TyCon listTy) elemTy => do
      let elemTyName = case elemTy of
                           TyCon name => name
                           _ => fail "仅支持代数数据类型"
      -- 获取Generic实例的构造函数元数据
      genInfo <- getGeneric elemTyName
      let conNames = map (\con => con.name) genInfo.cons
      let conExprs = map (\n => IVar EmptyFC n) conNames
      check $ `(the (List ~(elemTy)) [~(conExprs)])
    _ => fail "目标类型必须是 List a"

colors : List Color
colors = getConsListGeneric

main : IO () 
main = do
  putStrLn "Colors:"
  traverse_ (\c => putStrLn $ "  " ++ show c) colors

这种方式需要依赖Generics.Derive模块，适合已经使用Generic接口进行序列化、反序列化等操作的项目。

内容的提问来源于stack exchange，提问作者Quaxton Hale