How does one define new computation over types of kind GHC.TypeLits.Nat
? I am hoping to be able to define a type family
type family WIDTH (n :: Nat) :: Nat
such that WIDTH 0 ~ 0
and WIDTH (n+1) ~ log2 n
How does one define new computation over types of kind GHC.TypeLits.Nat
? I am hoping to be able to define a type family
type family WIDTH (n :: Nat) :: Nat
such that WIDTH 0 ~ 0
and WIDTH (n+1) ~ log2 n
We can pattern match on any literal
Nat
, then recurse using built-in operations.