haskell - 为 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 与一元表示相比，它是一种更有效的表示和操作类型级自然值的方法。但是，我看不到如何定义 AbsDiff对于 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

但似乎有 no way to constrain a type family instance .这是有道理的，因为 constraints don't guide typeclass resolution , 和类型族大概工作类似。
有没有办法写出高效的 AbsDiff对于 GHC.TypeLits.Nat ?

Answer 1

我发现了一个相当不舒服的解决方法，涉及 Data.Type.Bool.If .这很不舒服，因为 If是严格而不是懒惰；如果 0 - 1 :: Nat花了很多工作来解决，或者如果它是一个错误而不是不可约，那么这将不是一个解决方案:

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

module Nat where

import GHC.TypeLits
import Data.Type.Bool

type AbsDiff :: Nat -> Nat -> Nat
type family AbsDiff x y where
  AbsDiff x y = If (x <=? y) (y - x) (x - y)