Writing AbsDiff for GHC.TypeLits.Nat

Question

With Peano-style type-level naturals, it's fairly easy to write an absolute difference type-level function (aka type family):

{-# 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 is a more efficient way to represent and manipulate the type-level naturals, compared to a unary representation. However, I don't see how to define AbsDiff for GHC.TypeLits.Nat without resorting to unary subtraction. GHC.TypeLits.CmpNat exists, and I could imagine using it like this (hypothetical syntax):

{-# 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

But there appears to be no way to constrain a type family instance. This makes sense, as constraints don't guide typeclass resolution, and type families presumably work similarly.

Is there any way to write an efficient AbsDiff for GHC.TypeLits.Nat?

Answer 1

I found a rather uncomfortable workaround involving Data.Type.Bool.If. It's uncomfortable because If is strict rather than lazy; if 0 - 1 :: Nat took much work to resolve, or if it were an error rather than irreducible, then this wouldn't be a solution:

{-# 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)

Answer 2

You can use a helper to control evaluation. Given:

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

resolution of AbsDiff 0 1 and AbsDiff 1 0 loop, as you expected, but AbsDiff' 0 1 and AbsDiff' 1 0 work fine, so this definition should work for you:

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