我在探索Haskell中的類型族，試圖建立我可以定義的類型級函數的複雜性。我想定義的mod封閉式級版本，像這樣：類型族實例中的約束

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-} 
import GHC.TypeLits 

type family Mod (m :: Nat) (n :: Nat) :: Nat where 
    n <= m => Mod m n = Mod (m - n) n 
    Mod m n = m

然而，編譯器（GHC 7.10.2）拒絕此，作爲第一個公式中的約束是不允許的。價值層面的守衛如何轉化爲類型層面？ Haskell目前甚至有可能嗎？

來源

2016-05-31 prophet-on-that

也許有'If'類型的級別函數？我認爲我看到了在某個地方使用過，但我不是圖書館專家... – chi

謝謝，你是絕對正確的，如果[Data.Type.Bool]存在（https://hackage.haskell.org /package/base/docs/Data-Type-Bool.html）。 –

接下來，我設法使用編譯成功的類型級別If來重寫'Mod'。但是，任何嘗試減少'Mod m n'形式的項都會導致堆棧溢出異常。調整_-freduction-depth_選項向我表明，GHC優先擴展表達式的「m-n」部分，但沒有意識到這可能永遠不可能。我將不得不深入研究_DataKinds_擴展以瞭解更多的行爲。 –

不是一個答案（我不認爲現在甚至還有一個可能），但爲了其他人（如我）的利益試圖回顧評論中的OP步驟。以下編譯，但快速使用會導致堆棧溢出。

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-} 
import GHC.TypeLits 
import Data.Type.Bool 

type family Mod (m :: Nat) (n :: Nat) :: Nat where 
    Mod m n = If (n <=? m) (Mod (m - n) n) m

的原因是，If本身只是一個普通的家庭類型和類型家庭的行爲是使用那些在右側前擴大自己的類型參數（渴望在某種意義上）開始。在這種情況下不幸的結果是Mod (m - n) n得到擴展，即使n <=? m爲假，因此堆棧溢出。

由於完全相同的原因，Data.Type.Bool中的邏輯運算符不會短路。鑑於

type family Bottom :: Bool where Bottom = Bottom

我們可以看到，False && Bottom和True || Bottom雙方掛斷。

編輯

以防萬一OP是一種家庭用所需的行爲只是有興趣（而不僅僅是有型家庭衛士的更普遍的問題）有是表達Mod的方式一種終止的方式：

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-} 
import GHC.TypeLits 

type Mod m n = Mod1 m n 0 m 

type family Mod1 (m :: Nat) (n :: Nat) (c :: Nat) (acc :: Nat) :: Nat where 
    Mod1 m n n acc = Mod1 m n 0 m 
    Mod1 0 n c acc = acc 
    Mod1 m n c acc = Mod1 (m - 1) n (c + 1) acc

來源

2016-07-28 21:55:09 Alec

類型族實例中的約束

回答

編輯

相關問題