haskell - 类型族实例中的约束

Question

我正在探索 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 中是否可行？

Answer 1

不是答案(我认为甚至还没有答案)，但为了其他人(比如我)的利益，他们试图在评论中追溯 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