我正在探索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目前甚至有可能吗？

---

不是一个答案（我不认为现在甚至还有可能），但为了其他人（如我）的利益，试图在评论中追溯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本身只是一个普通类型的家庭，类型家庭的行为首先是在使用右边的类型之前扩展它们的类型参数（在某种意义上是渴望的）。 在这种情况下不幸的结果是，即使n <=? m Mod (m - n) n得到扩展n <=? m n <=? m是错误的，因此堆栈溢出。

出于完全相同的原因， Data.Type.Bool的逻辑运算符不会短路。 特定

type family Bottom :: Bool where Bottom = Bottom

我们可以看到False && Bottom and True || 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

链接地址: http://www.djcxy.com/p/43143.html

上一篇: Constraints in type family instances

下一篇: Haskell GADT typesafe Evaluator: Constant term for more than one type.