在Idris中如何实现类型字符串化输出？含自定义记录类型场景

好问题！在Idris里完全可以实现类似Haskell中show Type或typeOf的功能，甚至能自定义类型的字符串表示——包括你提到的记录类型。下面我一步步给你拆解实现方式：

核心思路：利用Idris的反射功能 #

Idris的类型在编译时是静态的，但通过启用反射扩展，我们可以把类型的结构带到运行时，再转换成你想要的字符串格式。首先要开启反射：

%language Reflection

第一步：实现通用的类型转字符串函数 #

我们先写一个函数，把Type（编译时类型）转换成它的运行时表示TypeRep，再通过模式匹配TypeRep来生成不同类型的字符串：

-- 处理TypeRep生成自定义格式的字符串
showTypeRep : TypeRep -> String
-- 处理基本类型（如Int、String）
showTypeRep (TRCon _ (UN name) []) = name
-- 处理带参数的类型（如List Int、Maybe String）
showTypeRep (TRCon _ (UN name) args) = name ++ " (" ++ unwords (map showTypeRep args) ++ ")"
-- 处理记录类型，生成你想要的{ field : Type, ... }格式
showTypeRep (TRRec _ (UN _) fields) = 
  "{ " ++ unwords (intersperse ", " (map showField fields)) ++ " }"
  where
    showField : (Name, TypeRep) -> String
    showField (UN fieldName, ty) = fieldName ++ " : " ++ showTypeRep ty
-- 处理函数类型
showTypeRep (TRFun arg ret) = showTypeRep arg ++ " -> " ++ showTypeRep ret
-- 其他类型 fallback 到默认显示
showTypeRep other = show other

-- 对外暴露的函数：输入Type，输出字符串
showType : Type -> String
showType t = showTypeRep (reflectType t)

第二步：测试自定义记录类型 #

现在定义你提到的Person记录，直接用showType就能得到想要的结果：

record Person where
  constructor Person
  name : String
  age : Int

-- 测试案例
testPersonType : String
testPersonType = showType Person  -- 结果就是 "{ name : String, age : Int }"

testBasicType : String
testBasicType = showType Int  -- 结果是 "Int"

testFunctionType : String
testFunctionType = showType (String -> Int -> Person)  -- 结果是 "String -> Int -> { name : String, age : Int }"

如果你想通过构造函数获取类型字符串 #

你的例子里提到调用myFunction Person（Person是构造函数），我们可以写一个辅助函数，自动提取构造函数的返回类型并转换：

-- 递归提取函数的返回类型
getReturnType : Type -> Type
getReturnType (arg -> ret) = getReturnType ret
getReturnType t = t

-- 接受任意构造函数，返回其对应类型的字符串
myFunction : {a : Type} -> a -> String
myFunction {a} _ = showType (getReturnType a)

-- 调用测试
testMyFunction : String
testMyFunction = myFunction Person  -- 同样得到 "{ name : String, age : Int }"

对比Haskell的泛型实现 #

如果习惯Haskell的泛型自动推导，Idris也支持Generic接口（在Data.Generic模块），可以自动为记录生成实例后实现通用的类型展示。不过对于这种类型字符串生成的需求，直接用反射会更直观灵活。

内容的提问来源于stack exchange，提问作者Nikita Tchayka