让 GHC 在“KnownNat”上应用基本的数学法则

问题描述

我刚刚从 hmatrix 包中发现了超级棒的 Haskell 库 Numeric.Linearalgebra.Static。

现在我实现了一个函数，将矩阵 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)) 之类的？

解决方法

有类型检查插件可以做到这一点。具体来说，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 约束是不可避免的。