Definizione di famiglie di tipi personalizzati rispetto al tipo Nat

Question

Come si può definire un nuovo calcolo su tipi di tipi GHC.TypeLits.Nat? Spero di essere in grado di definire un tipo di famiglia

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

tale che WIDTH 0 ~ 0 e WIDTH (n+1) ~ log2 n

Answer 1

possiamo abbinare modello su qualsiasi letterale Nat, quindi ricorsivamente utilizzando le operazioni incorporati.

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