type-level-tf-0.2.1: src/Data/TypeLevel/Num/Ops.hs
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, TypeOperators,
FlexibleInstances, FlexibleContexts, UndecidableInstances,
EmptyDataDecls, TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module : Data.TypeLevel.Num.Ops
-- Copyright : (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
-- and KTH's SAM group
-- License : BSD-style (see the file LICENSE)
--
-- Maintainer : alfonso.acosta@gmail.com
-- Stability : experimental
-- Portability : non-portable (MPTC, non-standard instances)
--
-- Type-level numerical operations and its value-level reflection functions.
--
----------------------------------------------------------------------------
module Data.TypeLevel.Num.Ops
(
-- * Successor/Predecessor
Succ, succ,
Pred, pred,
-- * Addition/Subtraction
Add, (+),
Sub, (-),
-- * Multiplication/Division
Mul, (*),
Div, div,
Mod, mod,
--DivMod, divMod,
IsDivBy, isDivBy,
-- ** Special efficiency cases
Mul10, mul10,
Div10, div10,
DivMod10, divMod10,
-- * Exponientiation/Logarithm
ExpBase, (^),
-- Not implemented
-- LogBase, logBase,
-- LogBaseF, logBaseF,
-- IsPowOf, isPowOf,
-- ** Special efficiency cases
Exp10, exp10,
Log10, log10,
-- * Comparison assertions
-- ** General comparison assertion
Trich, trich,
-- *** Type-level values denoting comparison results
LT, EQ, GT,
OrderingEq, NatEq,
-- ** Abbreviated comparison assertions
(:>:), (:<:), (:>=:), (:<=:),
(>) , (<) , (>=) , (<=),
-- * Maximum/Minimum
Max, max,
Min, min,
-- * Greatest Common Divisor
GCD, gcd
)
where
import Data.TypeLevel.Num.Reps
import Data.TypeLevel.Num.Sets
import Data.TypeLevel.Bool
import Prelude hiding
(succ, pred, (+), (-), (*), div, mod, divMod, (^), logBase,
(==), (>), (<), (<), (>=), (<=), max, min, gcd, Bool)
-------------------------
-- Successor, Predecessor
-------------------------
-- | Successor type-level relation. @Succ x y@ establishes
-- that @succ x = y@.
-- Assoc notes: Cannot avoid malformed types
type family Succ n
type instance Succ D0 = D1
type instance Succ D1 = D2
type instance Succ D2 = D3
type instance Succ D3 = D4
type instance Succ D4 = D5
type instance Succ D5 = D6
type instance Succ D6 = D7
type instance Succ D7 = D8
type instance Succ D8 = D9
type instance Succ D9 = (D1 :* D0)
type instance Succ (x:*D0) = (x:*D1)
type instance Succ (x:*D1) = (x:*D2)
type instance Succ (x:*D2) = (x:*D3)
type instance Succ (x:*D3) = (x:*D4)
type instance Succ (x:*D4) = (x:*D5)
type instance Succ (x:*D5) = (x:*D6)
type instance Succ (x:*D6) = (x:*D7)
type instance Succ (x:*D7) = (x:*D8)
type instance Succ (x:*D8) = (x:*D9)
type instance Succ (x:*D9) = (Succ x:*D0)
-- | value-level reflection function for the 'Succ' type-level relation
succ :: x -> Succ x
succ = undefined
type family Pred n
type instance Pred D1 = D0
type instance Pred D2 = D1
type instance Pred D3 = D2
type instance Pred D4 = D3
type instance Pred D5 = D4
type instance Pred D6 = D5
type instance Pred D7 = D6
type instance Pred D8 = D7
type instance Pred D9 = D8
type instance Pred (D1:*D0) = D9
type instance Pred (D2:*D0) = (D1:*D9)
type instance Pred (D3:*D0) = (D2:*D9)
type instance Pred (D4:*D0) = (D3:*D9)
type instance Pred (D5:*D0) = (D4:*D9)
type instance Pred (D6:*D0) = (D5:*D9)
type instance Pred (D7:*D0) = (D6:*D9)
type instance Pred (D8:*D0) = (D7:*D9)
type instance Pred (D9:*D0) = (D8:*D9)
type instance Pred (xd:*xm:*D0) = Pred(xd:*xm):*D9
type instance Pred (xd:*D1) = (xd:*D0)
type instance Pred (xd:*D2) = (xd:*D1)
type instance Pred (xd:*D3) = (xd:*D2)
type instance Pred (xd:*D4) = (xd:*D3)
type instance Pred (xd:*D5) = (xd:*D4)
type instance Pred (xd:*D6) = (xd:*D5)
type instance Pred (xd:*D7) = (xd:*D6)
type instance Pred (xd:*D8) = (xd:*D7)
type instance Pred (xd:*D9) = (xd:*D8)
pred :: x -> Pred x
pred = undefined
--
----------------------
---- Add and Subtract
----------------------
--
type family Div10 m
type instance Div10 D0 = D0
type instance Div10 D1 = D0
type instance Div10 D2 = D0
type instance Div10 D3 = D0
type instance Div10 D4 = D0
type instance Div10 D5 = D0
type instance Div10 D6 = D0
type instance Div10 D7 = D0
type instance Div10 D8 = D0
type instance Div10 D9 = D0
type instance Div10 (x:*D0) = x
type instance Div10 (x:*D1) = x
type instance Div10 (x:*D2) = x
type instance Div10 (x:*D3) = x
type instance Div10 (x:*D4) = x
type instance Div10 (x:*D5) = x
type instance Div10 (x:*D6) = x
type instance Div10 (x:*D7) = x
type instance Div10 (x:*D8) = x
type instance Div10 (x:*D9) = x
div10 :: x -> Div10 x
div10 = undefined
type family Mod10 n
type instance Mod10 D0 = D0
type instance Mod10 D1 = D1
type instance Mod10 D2 = D2
type instance Mod10 D3 = D3
type instance Mod10 D4 = D4
type instance Mod10 D5 = D5
type instance Mod10 D6 = D6
type instance Mod10 D7 = D7
type instance Mod10 D8 = D8
type instance Mod10 D9 = D9
type instance Mod10 (xd:*xm) = xm
mod10 :: x -> Mod10 x
mod10 = undefined
type family DivMod10 n
type instance DivMod10 n = (Div10 n, Mod10 n)
type family Add m n :: *
type instance Add D0 x = x
type instance Add D1 x = (Succ x)
type instance Add D2 x = Add D1 (Succ x)
type instance Add D3 x = Add D2 (Succ x)
type instance Add D4 x = Add D3 (Succ x)
type instance Add D5 x = Add D4 (Succ x)
type instance Add D6 x = Add D5 (Succ x)
type instance Add D7 x = Add D6 (Succ x)
type instance Add D8 x = Add D7 (Succ x)
type instance Add D9 x = Add D8 (Succ x)
type instance Add (xd :* xm) y = Add xm ((Add xd (Div10 y)) :* (Mod10 y))
-- | value-level reflection function for the 'Add' type-level relation
(+) :: x -> y -> Add x y
(+) = undefined
-- --| Subtraction type-level relation. @Sub x y z@ establishes
-- -- that @x - y = z@
type family Sub x y
type instance Sub x D0 = x
type instance Sub x D1 = (Pred x)
type instance Sub x D2 = Sub (Pred x) D1
type instance Sub x D3 = Sub (Pred x) D2
type instance Sub x D4 = Sub (Pred x) D3
type instance Sub x D5 = Sub (Pred x) D4
type instance Sub x D6 = Sub (Pred x) D5
type instance Sub x D7 = Sub (Pred x) D6
type instance Sub x D8 = Sub (Pred x) D7
type instance Sub x D9 = Sub (Pred x) D8
type instance Sub x (xd :* xm) = Sub (Pred x) (Pred (xd:*xm))
-- | value-level reflection function for the 'Sub' type-level relation
(-) :: x -> y -> Sub x y
(-) = undefined
--
--------------------------------
---- Multiplication and Division
--------------------------------
--
-------------------
---- Multiplication
-------------------
--
---- | Multiplication type-level relation. @Mul x y z@ establishes
---- that @x * y = z@.
type family Mul m n
type instance Mul D0 y = D0
type instance Mul D1 y = y
type instance Mul D2 y = Add y y
type instance Mul D3 y = Add y (Mul D2 y)
type instance Mul D4 y = Add y (Mul D3 y)
type instance Mul D5 y = Add y (Mul D4 y)
type instance Mul D6 y = Add y (Mul D5 y)
type instance Mul D7 y = Add y (Mul D6 y)
type instance Mul D8 y = Add y (Mul D7 y)
type instance Mul D9 y = Add y (Mul D8 y)
-- Note that this is only valid if xd is positive.
type instance Mul (xd :* xm) y = Add (Mul xm y) ((Mul xd y) :* D0)
-- | value-level reflection function for the multiplication type-level relation
(*) :: x -> y -> Mul x y
(*) = undefined
--
--
-------------
---- Division
-------------
-- | Division and Remainder type-level relation. @DivMod x y q r@ establishes
-- that @x/y = q + r/y@
-- division + modulo
-- x/y | y > x = (0,x)
-- x/y | y <= x = ( 1 + (x-y / y), mod (x - y))
-- This doesn't work
--type instance Div x y = Cond (y :>: x) D0 (Succ (Div (Sub x y) y))
--type instance Mod x y = Cond (y :>: x) x (Mod (Sub x y) y)
type family Div' x y x_gt_y
type instance Div' x y False = D0
type instance Div' x y True = Succ (Div' (Sub x y) y ((Sub x y) :>=: y))
type family Div x y
type instance Div x y = Div' x y (Trich x y)
type family Mod' x y x_gt_y
type instance Mod' x y False = x
type instance Mod' x y True = Mod' (Sub x y) y ((Sub x y) :>=: y)
type family Mod x y
type instance Mod x y = Mod' x y (x :>=: y)
-- | value-level reflection function for the 'DivMod' type-level relation
divMod :: x -> y -> (Div x y, Mod x y)
divMod _ _ = (undefined)
-- | value-level reflection function for the 'Div' type-level relation
div :: x -> y -> Div x y
div = undefined
-- | value-level reflection function for the 'Mod' type-level relation
mod :: x -> y -> Mod x y
mod = undefined
------------------------------------------
---- Multiplication/Division special cases
------------------------------------------
-- | Multiplication by 10 type-level relation (based on 'DivMod10').
-- @Mul10 x y@ establishes that @10 * x = y@.
type family Mul10 n
type instance Mul10 x = (x :* D0)
-- | value-level reflection function for 'Mul10'
mul10 :: x -> Mul10 x
mul10 = undefined
---- | value-level reflection function for DivMod10
divMod10 :: x -> (Div10 x, Mod10 x)
divMod10 _ = (undefined, undefined)
--
------------------------------
---- Is-Divisible-By assertion
------------------------------
-- | Is-divisible-by type-level assertion. e.g @IsDivBy d x@ establishes that
-- @x@ is divisible by @d@.
-- here we use a class for demonstration purposes
class (Pos d, Nat x) => IsDivBy d x
instance (Pos d, Nat x, Mod x d ~ D0) => IsDivBy d x
-- | value-level reflection function for IsDivBy
isDivBy :: IsDivBy d x => d -> x -> ()
isDivBy _ _ = ()
-----------------------------
---- Exponentiation/Logarithm
-----------------------------
--
---- | Exponentation type-level relation. @ExpBase b e r@ establishes
---- that @b^e = r@
type family ExpBase b e
type instance ExpBase b D0 = D1
type instance ExpBase b D1 = b
type instance ExpBase b D2 = (Mul b b)
type instance ExpBase b D3 = (Mul b (ExpBase b D2))
type instance ExpBase b D4 = (Mul b (ExpBase b D3))
type instance ExpBase b D5 = (Mul b (ExpBase b D4))
type instance ExpBase b D6 = (Mul b (ExpBase b D5))
type instance ExpBase b D7 = (Mul b (ExpBase b D6))
type instance ExpBase b D8 = (Mul b (ExpBase b D7))
type instance ExpBase b D9 = (Mul b (ExpBase b D8))
type instance ExpBase b (ei :* el) = Mul b (ExpBase b (Pred (ei:* el)))
-- | value-level reflection function for the ExpBase type-level relation
(^) :: b -> e -> ExpBase b e
(^) = undefined
---------------- LEFT OUT FOR NOW ---------------------------------
-- Logarithm type-level relation. @LogBase b x e@ establishes that
-- @log_base_b x = e@
-- Note it is not relational (i.e. cannot be used to express exponentiation)
--class (Pos b, b :>=: D2, Pos x, Nat e) => LogBase b x e | b x -> e
--instance LogBaseF b x e f => LogBase b x e
--
--
---- | value-level reflection function for LogBase
--logBase :: LogBaseF b x e f => b -> x -> e
--logBase = undefined
--
--
---- | Version of LogBase which also outputs if the logarithm
---- calculated was exact.
---- f indicates if the resulting logarithm has no fractional part (i.e.
---- tells if the result provided is exact)
--class (Pos b, b :>=: D2, Pos x, Nat e, Bool f)
-- => LogBaseF b x e f | b x -> e f
--instance (Trich x b cmp, LogBaseF' b x e f cmp) => LogBaseF b x e f
--
--
--class (Pos b, b :>=: D2, Pos x, Nat e, Bool f)
-- => LogBaseF' b x e f cmp | b x cmp -> e f
--instance (Pos b, b :>=: D2, Pos x) => LogBaseF' b x D0 False LT
--instance (Pos b, b :>=: D2) => LogBaseF' b b D1 True EQ
--instance (Pos b, b :>=: D2, Pos x, DivMod x b q r, IsZero r rz, And rz f' f,
-- Pred e e', LogBaseF b q e' f') => LogBaseF' b x e f GT
--
---- | value-level reflection function for LogBaseF
--logBaseF :: LogBaseF b x e f => b -> x -> (e,f)
--logBaseF _ _ = (undefined, undefined)
--
-- We could reuse LogBaseF for IsPowOf but it would be inneficient.
-- LogBaseF continues calculating the logarithm even if after knowing its
-- not exact. Thus, it is desirable to include a custom definition of
-- IsPowOf which can "abort" the calculation forcing the Divisions to be
-- exact
-- | Assert that a number (@x@) can be expressed as the power of another one
-- (@b@) (i.e. the fractional part of @log_base_b x = 0@, or,
-- in a different way, @exists y . b\^y = x@).
--
--class (Pos b, b :>=: D2, Pos x) => IsPowOf b x
--instance (Trich x b cmp, IsPowOf' b x cmp) => IsPowOf b x
--class (Pos b, b :>=: D2, Pos x) => IsPowOf' b x cmp
---- If lower (x < b), then the logarithm is not exact
---- instance (Pos b, b :>=: D2, Pos x) => IsPowOf' b x LT
--instance (Pos b, b :>=: D2) => IsPowOf' b b EQ
--instance (Pos b, b :>=: D2, Pos x, DivMod x b q D0, IsPowOf b q)
-- => IsPowOf' b x GT
---- |
--isPowOf :: IsPowOf b x => b -> x -> ()
--isPowOf = undefined
-------------------------------------
---- Base-10 Exponentiation/Logarithm
-------------------------------------
type family Exp10 x
type instance Exp10 D0 = D1
type instance Exp10 D1 = (D1 :* D0)
type instance Exp10 D2 = (D1 :* D0 :* D0)
type instance Exp10 D3 = (D1 :* D0 :* D0 :* D0)
type instance Exp10 D4 = (D1 :* D0 :* D0 :* D0 :* D0)
type instance Exp10 D5 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0)
type instance Exp10 D6 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
type instance Exp10 D7 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
type instance Exp10 D8 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
type instance Exp10 D9 = (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
type instance Exp10 (xi :* xl) = (Exp10 (Pred (xi:*xl)) :* D0)
-- | value-level reflection function for Exp10
exp10 :: x -> Exp10 x
exp10 = undefined
-- | Base-10 logarithm type-level relation
-- Note it is not relational (cannot be used to express Exponentation to 10)
-- However, it works with any positive numeral (not just powers of 10)
type family Log10 x
type instance Log10 D1 = D0
type instance Log10 D2 = D0
type instance Log10 D3 = D0
type instance Log10 D4 = D0
type instance Log10 D5 = D0
type instance Log10 D6 = D0
type instance Log10 D7 = D0
type instance Log10 D8 = D0
type instance Log10 D9 = D0
type instance Log10 (xi :* xl) = Pred (Log10 xi)
-- | value-level reflection function for 'Log10'
log10 :: x -> Log10 x
log10 = undefined
--
--{- Log10': Alternative implementation of Log10
--
--Relational, but it only works for results of Exp10 (i.e. powers of 10).
--
--class (Pos x, Nat y) => Log10' x y | x -> y, y -> x
--instance Exp10 x y => Log10' y x
---}
--
--
---------------
---- Comparison
---------------
-- type-level values denoting comparison results
-- | Lower than
data LT
-- | Equal
data EQ
-- | Greater than
data GT
type family OrderingEq o1 o2
type instance OrderingEq LT LT = True
type instance OrderingEq LT EQ = False
type instance OrderingEq LT GT = False
type instance OrderingEq EQ EQ = True
type instance OrderingEq EQ LT = False
type instance OrderingEq EQ GT = False
type instance OrderingEq GT GT = True
type instance OrderingEq GT LT = False
type instance OrderingEq GT EQ = False
-- | Trichotomy type-level relation. 'Trich x y r' establishes
-- the relation (@r@) between @x@ and @y@. The obtained relation (@r@)
-- Can be 'LT' (if @x@ is lower than @y@), 'EQ' (if @x@ equals @y@) or
-- 'GT' (if @x@ is greater than @y@)
type family Trich x y
-- | value-level reflection function for the comparison type-level assertion
trich :: x -> y -> Trich x y
trich = undefined
-- by structural induction on the first, and then the second argument
-- D0
type instance Trich D0 D0 = EQ
type instance Trich D0 D1 = LT
type instance Trich D0 D2 = LT
type instance Trich D0 D3 = LT
type instance Trich D0 D4 = LT
type instance Trich D0 D5 = LT
type instance Trich D0 D6 = LT
type instance Trich D0 D7 = LT
type instance Trich D0 D8 = LT
type instance Trich D0 D9 = LT
type instance Trich D0 (yi :* yl) = LT
type instance Trich (yi :* yl) D0 = GT
-- D1
type instance Trich D1 D0 = GT
type instance Trich D1 D1 = EQ
type instance Trich D1 D2 = LT
type instance Trich D1 D3 = LT
type instance Trich D1 D4 = LT
type instance Trich D1 D5 = LT
type instance Trich D1 D6 = LT
type instance Trich D1 D7 = LT
type instance Trich D1 D8 = LT
type instance Trich D1 D9 = LT
type instance Trich D1 (yi :* yl) = LT
type instance Trich (yi :* yl) D1 = GT
-- D2
type instance Trich D2 D0 = GT
type instance Trich D2 D1 = GT
type instance Trich D2 D2 = EQ
type instance Trich D2 D3 = LT
type instance Trich D2 D4 = LT
type instance Trich D2 D5 = LT
type instance Trich D2 D6 = LT
type instance Trich D2 D7 = LT
type instance Trich D2 D8 = LT
type instance Trich D2 D9 = LT
type instance Trich D2 (yi :* yl) = LT
type instance Trich (yi :* yl) D2 = GT
-- D3
type instance Trich D3 D0 = GT
type instance Trich D3 D1 = GT
type instance Trich D3 D2 = GT
type instance Trich D3 D3 = EQ
type instance Trich D3 D4 = LT
type instance Trich D3 D5 = LT
type instance Trich D3 D6 = LT
type instance Trich D3 D7 = LT
type instance Trich D3 D8 = LT
type instance Trich D3 D9 = LT
type instance Trich D3 (yi :* yl) = LT
type instance Trich (yi :* yl) D3 = GT
-- D4
type instance Trich D4 D0 = GT
type instance Trich D4 D1 = GT
type instance Trich D4 D2 = GT
type instance Trich D4 D3 = GT
type instance Trich D4 D4 = EQ
type instance Trich D4 D5 = LT
type instance Trich D4 D6 = LT
type instance Trich D4 D7 = LT
type instance Trich D4 D8 = LT
type instance Trich D4 D9 = LT
type instance Trich D4 (yi :* yl) = LT
type instance Trich (yi :* yl) D4 = GT
-- D5
type instance Trich D5 D0 = GT
type instance Trich D5 D1 = GT
type instance Trich D5 D2 = GT
type instance Trich D5 D3 = GT
type instance Trich D5 D4 = GT
type instance Trich D5 D5 = EQ
type instance Trich D5 D6 = LT
type instance Trich D5 D7 = LT
type instance Trich D5 D8 = LT
type instance Trich D5 D9 = LT
type instance Trich D5 (yi :* yl) = LT
type instance Trich (yi :* yl) D5 = GT
-- D6
type instance Trich D6 D0 = GT
type instance Trich D6 D1 = GT
type instance Trich D6 D2 = GT
type instance Trich D6 D3 = GT
type instance Trich D6 D4 = GT
type instance Trich D6 D5 = GT
type instance Trich D6 D6 = EQ
type instance Trich D6 D7 = LT
type instance Trich D6 D8 = LT
type instance Trich D6 D9 = LT
type instance Trich D6 (yi :* yl) = LT
type instance Trich (yi :* yl) D6 = GT
-- D7
type instance Trich D7 D0 = GT
type instance Trich D7 D1 = GT
type instance Trich D7 D2 = GT
type instance Trich D7 D3 = GT
type instance Trich D7 D4 = GT
type instance Trich D7 D5 = GT
type instance Trich D7 D6 = GT
type instance Trich D7 D7 = EQ
type instance Trich D7 D8 = LT
type instance Trich D7 D9 = LT
type instance Trich D7 (yi :* yl) = LT
type instance Trich (yi :* yl) D7 = GT
-- D8
type instance Trich D8 D0 = GT
type instance Trich D8 D1 = GT
type instance Trich D8 D2 = GT
type instance Trich D8 D3 = GT
type instance Trich D8 D4 = GT
type instance Trich D8 D5 = GT
type instance Trich D8 D6 = GT
type instance Trich D8 D7 = GT
type instance Trich D8 D8 = EQ
type instance Trich D8 D9 = LT
type instance Trich D8 (yi :* yl) = LT
type instance Trich (yi :* yl) D8 = GT
-- D9
type instance Trich D9 D0 = GT
type instance Trich D9 D1 = GT
type instance Trich D9 D2 = GT
type instance Trich D9 D3 = GT
type instance Trich D9 D4 = GT
type instance Trich D9 D5 = GT
type instance Trich D9 D6 = GT
type instance Trich D9 D7 = GT
type instance Trich D9 D8 = GT
type instance Trich D9 D9 = EQ
type instance Trich D9 (yi :* yl) = LT
type instance Trich (yi :* yl) D9 = GT
-- multidigit comparison
type instance Trich (xd :* xm) (yd :* ym) = CS (Trich xd yd) (Trich xm ym)
-- strengthen the comparison relation
type family CS c1 c2
type instance CS EQ r = r
type instance CS GT r = GT
type instance CS LT r = LT
-- Abbreviated comparison assertions
-- | Equality abbreviated type-level assertion
type family NatEq x y
type instance NatEq x y = OrderingEq (Trich x y) EQ
-- | Greater-than abbreviated type-level assertion
type family x :>: y
type instance x :>: y = OrderingEq (Trich x y) GT
-- | value-level reflection function for >
(>) :: x -> y -> x :>: y
(>) = undefined
-- | Lower-than abbreviated type-level assertion
type family x :<: y
type instance x :<: y = OrderingEq (Trich x y) LT
-- | value-level reflection function for >
(<) :: x -> y -> x :<: y
(<) = undefined
-- | Greater-than or equal abbreviated type-level assertion
type family x :>=: y
type instance x :>=: y = (Succ x) :>: y
-- | value-level reflection function for >=
(>=) :: x -> y -> x :>=: y
(>=) = undefined
-- | Less-than or equal abbreviated type-level assertion
type family x :<=: y
type instance x :<=: y = x :<: (Succ y)
-- | value-level reflection function for >=
(<=) :: x -> y -> x :<=: y
(<=) = undefined
--------------------
---- Maximum/Minimum
--------------------
type family Max x y
type instance Max x y = Cond (x :>: y) x y
type family Min x y
type instance Min x y = Cond (x :<=: y) x y
-- | value-level reflection function for the maximum type-level relation
max :: x -> y -> Max x y
max = undefined
-- | value-level reflection function for the minimum type-level relation
min :: x -> y -> Min x y
min = undefined
---------
---- GCD
---------
-- | Greatest Common Divisor type-level relation
type family GCD x y
type instance GCD x y = GCD' x y (IsZero y) (Trich x y)
---- Euclidean algorithm
--class (Nat x, Nat y, Nat gcd) => GCD' x y yz cmp gcd | x y yz cmp -> gcd
type family GCD' x y ys cmp
type instance GCD' x D0 True cmp = D0
type instance GCD' x y False LT = GCD y x
type instance GCD' x y False EQ = x
type instance GCD' x y False GT = GCD (Sub x y) y
-- | value-level reflection function for the GCD type-level relation
gcd :: x -> y -> GCD x y
gcd = undefined
-----------------------
---- Internal functions
-----------------------
--
-- classify a natural as positive or zero
type family IsZero n
type instance IsZero D0 = True
type instance IsZero D1 = False
type instance IsZero D2 = False
type instance IsZero D3 = False
type instance IsZero D4 = False
type instance IsZero D5 = False
type instance IsZero D6 = False
type instance IsZero D7 = False
type instance IsZero D8 = False
type instance IsZero D9 = False
-- debatable
type instance IsZero (xd:*xm) = And (IsZero xd) (IsZero xm)
--
-- The cond TF
type family Cond b x y
type instance Cond True x y = x
type instance Cond False x y = y