Nat türünde özel tip ailelerin tanımlanması

Question

Tür, GHC.TypeLits.Nat türlerine göre nasıl yeni bir hesaplama tanımlar? Bir tür aileyi tanımlayabilecek umuyorum

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

öyle ki WIDTH 0 ~ 0 ve WIDTH (n+1) ~ log2 n

Answer 1

Biz gelen her literal Nat üzerine desen maçının ardından yerleşik işlemlerini kullanarak Recurse.

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