类型族实例中的约束

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

这不是一个答案（我认为还没有一个可能），但为了其他人（比如我）试图在评论中追溯操作步骤的利益。以下代码可以编译，但使用它很快就会导致堆栈溢出。

{-# 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 <=? mfalse，也会被扩展，从而导致堆栈溢出。

出于完全相同的原因， 中的逻辑运算符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