haskell - 让 GHC 在 `KnownNat` 上应用基本的数学定律

Question

我刚刚发现了 super 棒的 Haskell 库 Numeric.LinearAlgebra.Static来自 hmatrix包裹。
现在我实现了一个函数，它将矩阵 A 转换为向量 B 和另一个矩阵 C，如下所示:

    1 2 3
A = 4 5 6
    7 8 9

B = 2 3

C = 5 6
    8 9

我想出的成功编译的代码如下所示:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}

import GHC.TypeLits
import Numeric.LinearAlgebra.Static

f :: (KnownNat (n + 1), KnownNat n, 1 <= n + 1, ((n + 1) - 1) ~ n)
  => Sq (n + 1) -> (R n, Sq n)
f m = (unrow a, b)
    where
        (a, b) = splitRows . snd . splitCols $ m

main :: IO ()
main = print $ f $ (matrix [1, 2, 3, 4, 5, 6, 7, 8, 9] :: Sq 3)

现在这很好用，但我希望我可以删除看似多余的东西，如 ((n + 1) - 1) ~ n从类型签名。
是否有可能让 GHC 接受像 f :: Sq (n + 1) -> (R n, Sq n) 这样的签名？没有别的？或者至少像 f :: (KnownNat n, 2 <= n) => Sq n -> (R (n - 1), Sq (n - 1)) ?

Answer 1

有类型检查插件可以做到这一点。具体来说，ghc-typelits-natnormalise可以算出((n + 1) - 1) ~ n和 1 <= n + 1 , 而 ghc-typelits-knownnat可以算出KnownNat n暗示 KnownNat (n+1) .因此，安装了两个软件包后，您可以编写:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

import GHC.TypeLits
import Numeric.LinearAlgebra.Static

f :: (KnownNat n) => Sq (n + 1) -> (R n, Sq n)
f m = (unrow a, b)
    where
        (a, b) = splitRows . snd . splitCols $ m

main :: IO ()
main = print $ f $ (matrix [1, 2, 3, 4, 5, 6, 7, 8, 9] :: Sq 3)

KnownNat n约束是不可避免的。