如何将Haskell类型族转换为等价的Idris类型函数？

Idris 不支持直接对 Type 类型的参数做模式匹配，因此不能像 Haskell 类型族那样直接写顶层的类型匹配函数。我们可以把类型映射和转换逻辑封装到 Idris 接口中，用接口关联类型实现等价的类型映射功能，完整实现如下：

1. 定义基础求和类型 #

对应 Haskell 中的 :+: 类型：

data (:+:) : Type -> Type -> Type where
  (:+:) : a -> b -> a :+: b

2. 定义封装类型映射和转换的接口 #

用接口关联类型替代 Haskell 顶层类型族，同时把转换方法声明在接口中：

interface HasConvert a where
  -- 对应 Haskell 的 MapType 类型族，作为接口的关联类型
  MapType : Type
  -- 转换方法，Idris 不需要额外的 Proxy 传递类型信息
  convert : a -> MapType

3. 实现各类型的接口实例 #

基础类型实例 #

HasConvert Int where
  MapType = Integer
  convert = cast

HasConvert Integer where
  MapType = Integer
  convert = id

求和类型实例 #

对应 Haskell 的多参数实例约束，用显式类型应用指定关联类型所属的类型参数：

(HasConvert a, HasConvert b) => HasConvert (a :+: b) where
  MapType = (MapType @a, MapType @b)
  convert (a :+: b) = (convert a, convert b)

使用示例 #

sample : Int :+: Integer
sample = 12 :+: 34

-- 运行 convert sample 会得到 (12, 34)，类型为 (Integer, Integer)

该实现和原 Haskell 逻辑完全等价，且符合 Idris 的类型系统规则，不会出现类型模式匹配报错。

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