我在探索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

类型族实例中的约束

回答

编辑

相关问题