10

与 GHC 的 DataKinds 混在一起，我尝试实现类型级二进制 nats。它们很容易实现，但是如果我希望它们在常见情况下有用，那么 GHC 需要相信Succ类型族是单射的（因此类型推断至少与一元类型级别一样有效纳特）。但是，我很难说服 GHC 就是这种情况。考虑以下二进制 nat 的编码：

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilyDependencies #-}
module Nat2 where

data Nat = Zero | Pos Nat1
data Nat1 = One | Bit0 Nat1 | Bit1 Nat1
  -- by separating Nat and Nat1 we avoid dealing w/ Bit0^n Zero as a spurrious representation of 0

type family Succ (n :: Nat) :: r | r -> n where
  Succ 'Zero = 'Pos 'One
  Succ ('Pos x) = 'Pos (Succ1 x)

type family Succ1 (n :: Nat1) :: r | r -> n where
  Succ1 'One = 'Bit0 'One
  Succ1 ('Bit0 x) = 'Bit1 x
  Succ1 ('Bit1 x) = 'Bit0 (Succ1 x)

GHC 无法接受这一点，因为它无法判断这Succ1是单射的：

Nat2.hs:12:3: error:
    • Type family equations violate injectivity annotation:
        Succ 'Zero = 'Pos 'One -- Defined at Nat2.hs:12:3
        Succ ('Pos x) = 'Pos (Succ1 x) -- Defined at Nat2.hs:13:3
    • In the equations for closed type family ‘Succ’
      In the type family declaration for ‘Succ’
   |
12 |   Succ 'Zero = 'Pos 'One
   |   ^^^^^^^^^^^^^^^^^^^^^^

Nat2.hs:16:3: error:
    • Type family equations violate injectivity annotation:
        Succ1 'One = 'Bit0 'One -- Defined at Nat2.hs:16:3
        Succ1 ('Bit1 x) = 'Bit0 (Succ1 x) -- Defined at Nat2.hs:18:3
    • In the equations for closed type family ‘Succ1’
      In the type family declaration for ‘Succ1’
   |
16 |   Succ1 'One = 'Bit0 'One
   |   ^^^^^^^^^^^^^^^^^^^^^^^

我们认为它是单射的，因为通过检查Succ1,One永远不会出现在它的形象中，所以Bit0 (Succ1 x)case 永远不会返回Bit0 One，因此Bit1case 永远不会与 case 冲突One。同样的论点（“One不在”的形象中Succ1）表明它Succ本身也是单射的。然而，GHC 还不够聪明，无法找到这个论点。

所以，问题：在这种情况下（以及类似的情况），有没有办法让 GHC 相信内射型家族实际上是内射的？（也许是一个类型检查器插件，我可以在其中提供一个反转 Succ1 的函数？也许是一个编译指示说“尝试从这个系列向后推断，就好像它是单射的；如果你遇到任何歧义，你就可以崩溃”？）

4

0 回答 0