Writing AbsDiff for GHC.TypeLits.Nat-CodePudding

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?

CodePudding user response：

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)

CodePudding user response：

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