为 GHC.TypeLits.Nat 编写 AbsDiff

Question

使用 Peano 风格的类型级自然数，编写绝对差类型级函数（也称为类型族）相当容易：

{-# LANGUAGE DataKinds, StandaloneKindSignatures, TypeFamilies #-}

module Nat where

data Nat = Z | S Nat

type AbsDiff :: Nat -> Nat -> Nat
type family AbsDiff x y where
  AbsDiff x Z = x
  AbsDiff Z y = y
  AbsDiff (S x) (S y) = AbsDiff x y

GHC.TypeLits.Nat与一元表示相比，是表示和操作类型级自然数的更有效方法。但是，我不知道如何在不诉诸一元减法的情况下定义AbsDifffor GHC.TypeLits.Nat。GHC.TypeLits.CmpNat存在，我可以想象像这样使用它（假设语法）：

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

module Nat

import GHC.TypeLits

type family AbsDiff x y where
  CmpNat x y ~ LT => AbsDiff x y = y - x
  CmpNat x y ~ EQ => AbsDiff x y = 0
  CmpNat x y ~ GT => AbsDiff x y = x - y

但似乎没有办法限制类型族实例。这是有道理的，因为约束不会指导类型类解析，并且类型族的工作原理可能类似。

有没有办法写一个高效的AbsDifffor GHC.TypeLits.Nat？

Answer 1

您可以使用助手来控制评估。鉴于：

type family Minus x y where
  Minus 1 0 = 1
  Minus 0 1 = Minus 0 1  -- infinite loop

type family AbsDiff x y where
  AbsDiff x y = If (x <=? y) (Minus y x) (Minus x y)

type family AbsDiff' x y where
  AbsDiff' x y = AbsDiff1 (x <=? y) x y
type family AbsDiff1 c x y where
  AbsDiff1 True x y = Minus y x
  AbsDiff1 False x y = Minus x y

AbsDiff 0 1和循环的解析AbsDiff 1 0，正如您所期望的，但是AbsDiff' 0 1和AbsDiff' 1 0工作正常，所以这个定义应该适合您：

type family AbsDiff' x y where
    AbsDiff' x y = AbsDiff1 (x <=? y) x y
type family AbsDiff1 c x y where
    AbsDiff1 True x y = y - x
    AbsDiff1 False x y = x - y