如何为GHC.TypeLits.Nat编写高效的AbsDiff类型级函数

可行实现方案 #

你可以通过辅助类型族对CmpNat的返回结果做模式匹配来实现分支逻辑，不需要在类型族实例上附加约束，完整的高效实现如下：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Nat where

import GHC.TypeLits (Nat, CmpNat, type (-))

type AbsDiff :: Nat -> Nat -> Nat
type family AbsDiff x y where
  AbsDiff x y = AbsDiffImpl (CmpNat x y) x y

type AbsDiffImpl :: Ordering -> Nat -> Nat -> Nat
type family AbsDiffImpl ord x y where
  AbsDiffImpl 'LT x y = y - x
  AbsDiffImpl 'EQ x y = 0
  AbsDiffImpl 'GT x y = x - y

实现说明 #

• 核心逻辑和你最初设想的完全一致，只是把约束分支转换成了对CmpNat返回的类型级Ordering构造子的模式匹配，符合GHC类型族的语法规则。
• 这个实现完全依赖GHC内置的GHC.TypeLits操作，不需要把Nat转换成Peano一元结构再做计算，效率和内置类型级Nat操作一致。
• 因为已经提前通过CmpNat判断了两个数的大小关系，调用减法时永远是大数减小数，不会触发GHC Nat减法的截断语义，结果完全正确。

你可以用下面的例子验证效果：

-- 测试用例，类型检查通过即表示计算正确
type Test1 = AbsDiff 3 5 ~ 2
type Test2 = AbsDiff 5 3 ~ 2
type Test3 = AbsDiff 7 7 ~ 0

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