有了Peano風格的型別級自然數，撰寫一個絕對差異的型別級函式（又稱型別族）是相當容易的：
{-# LANGUAGE DataKinds, StandaloneKindSignatures, TypeFamilies #-}
module Nat where
data Nat = Z | S Nat
type AbsDiff : 。Nat -> Nat -> Nat>
type family AbsDiff x y where
AbsDiff x Z = x
AbsDiff Z y = y
AbsDiff (S x) (S y) =AbsDiff x y
GHC.TypeLits.Nat與單數表示法相比，這是一種更有效的表示和操作型別級自然數的方法。然而，我不知道如何為GHC.TypeLits.Nat定義AbsDiff而不求助于單數減法。GHC.TypeLits.CmpNat存在，我可以想象這樣使用它（假設的語法）：
{-# LANGUAGE DataKinds, StandaloneKindSignatures, TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Nat
輸入GHC.TypeLits
type family AbsDiff x y where
CmpNat x y ~ LT => AbsDiff x y = y - x
CmpNat x y ~ EQ => AbsDiff x y = 0
CmpNat x y ~ GT => AbsDiff x y = x - y
但是似乎沒有辦法約束一個型別族實體
。這是有道理的，因為約束并不能指導型別族的決議，而型別族的作業原理應該是相似的。是否有辦法為GHC.TypeLits.Nat撰寫一個高效的AbsDiff？
uj5u.com熱心網友回復：
我發現了一個相當不舒服的作業方法，涉及Data.Type.Bool.If。不舒服是因為If是嚴格的而不是懶惰的；如果0 - 1 :: Nat需要很多作業來解決，或者如果它是一個錯誤而不是不可還原的，那么這就不是一個解決辦法：
{-# LANGUAGE DataKinds, PolyKinds, StandaloneKindSignatures, TypeFamilies #-}
{-# LANGUAGE TypeOperators, UndecidableInstances #-}
module Nat where
import GHC.TypeLits
import Data.Type.Bool
type AbsDiff :: Nat -> Nat -> Nat>
type family AbsDiff x y where
AbsDiff x y = If (x <=? y) (y - x) (x - y)
uj5u.com熱心網友回復：
你可以使用一個幫助器來控制評估。 給定：
type family Minus x y where
Minus 1 0 = 1
Minus 0 1 =Minus 0 1 --無限回圈
type family AbsDiff x y where
AbsDiff x y = If (x <=? y) (Minus y x) （Minus x y)
type family AbsDiff'/span> x y where
AbsDiff' x y = AbsDiff1 （x <=? y） x y
type family AbsDiff1 c x y where
AbsDiff1 True x y = Minus y x
AbsDiff1 False x y = Minus x y
AbsDiff 0 1和AbsDiff 1 0的解析度回圈，如你所料，但AbsDiff' 0 1和AbsDiff' 1 0作業正常，所以這個定義應該對你有用：
type family AbsDiff' x y where
AbsDiff' x y = AbsDiff1 （x <=? y） x y
type family AbsDiff1 c x y where
AbsDiff1 True x y = y - x
AbsDiff1 False x y = x - y
轉載請註明出處，本文鏈接：https://www.uj5u.com/qiye/329811.html
標籤：
上一篇：Haskell中的零階函式