Defining Custom Type Families Over a Nat View

Question

How to define a new calculation by type types GHC.TypeLits.Nat ? I hope I can define a type family

 type family WIDTH (n :: Nat) :: Nat 

such that WIDTH 0 ~ 0 and WIDTH (n+1) ~ log2 n

Answer 1

We can match patterns on any literal Nat , and then use built-in operations recursively.

 {-# LANGUAGE UndecidableInstances #-} import GHC.TypeLits type family Div2 n where Div2 0 = 0 Div2 1 = 0 Div2 n = Div2 (n - 2) + 1 type family Log2 n where Log2 0 = 0 -- there has to be a case, else we get nontermination -- or we could return Maybe Nat Log2 1 = 0 Log2 n = Log2 (Div2 n) + 1 type family WIDTH n where WIDTH 0 = 0 WIDTH n = Log2 (n - 1)