为何无法在Agda中定义Set→Set类型函数？如何实现类Haskell闭类型族映射？

首先定义四个基础类型：

data Q : Set where
  q1 : Q
  q2 : Q

data P : Set where
  p1 : P
  p2 : P

data C : Set where
  c1 : C
  c2 : C

data D : Set where 
  d1 : D 
  d2 : D

当尝试定义如下函数时，会触发unreachable clause警告：

f : Set -> Set
f D = Q
f P = C

这是因为Agda要求Set -> Set类型的函数必须覆盖所有Set类型的输入，但我们只需要指定D、P到Q、C的映射，这和Haskell封闭类型族的需求一致，以下是两种可行的实现方式：

方法1：基于索引数据类型的类型家族 #

通过定义一个枚举目标类型的索引类型，再基于该索引实现类型映射，完全符合Agda的函数完备性要求：

-- 枚举需要参与映射的类型标识
data TargetType : Set where
  DT : TargetType
  PT : TargetType

-- 将标识映射到实际的Set类型
TypeOf : TargetType -> Set
TypeOf DT = D
TypeOf PT = P

-- 定义目标类型映射，对应Haskell的封闭类型族
F : TargetType -> Set
F DT = Q
F PT = C

使用时，F DT会得到Q，F PT会得到C。如果需要扩展映射关系，只需给TargetType添加新构造子，并补全TypeOf和F的定义即可，和封闭类型族的扩展性逻辑一致。

方法2：利用Agda实例系统实现 #

如果希望更贴近Haskell类型族的使用体验，可以借助Agda的实例系统来实现：

-- 定义记录类型，描述两个类型的映射关系
record TypeMap (A B : Set) : Set where
  constructor mkTypeMap

-- 为需要的类型对定义实例
instance
  dToQ : TypeMap D Q
  dToQ = mkTypeMap

  pToC : TypeMap P C
  pToC = mkTypeMap

-- 通过实例查找自动推导映射后的类型
F : Set -> Set
F A = {B : Set} {{_ : TypeMap A B}} -> B

使用时，只要存在对应的TypeMap实例，F D会自动推导为Q，F P会推导为C。若传入没有对应实例的类型，Agda会直接报错，这和Haskell封闭类型族未覆盖类型时的行为一致。

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