haskell - 结合 `SomeNat` 和 `Nat`

Question

我正在遵循问题 Can I have an unknown KnownNat? 中列出的示例

我想对代码做一个小改动。

原来的代码是

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}

import GHC.TypeLits
import Data.Proxy

data Bar (n :: Nat) = Bar String deriving Show

bar :: (KnownNat n) => Bar n -> (String, Integer)
bar b@(Bar s) = (s, natVal b)

main :: IO ()
main = do
    i <- readLn
    let Just someNat = someNatVal i
    case someNat of
        SomeNat (_ :: Proxy n) -> do
            let a :: Bar n
                a = Bar "as"
            print $ bar a

它按预期工作。我想进行更改，修改类型级别 n .

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}

import GHC.TypeLits
import Data.Proxy

data Bar (n :: Nat) = Bar String deriving Show

bar :: (KnownNat n) => Bar n -> (String, Integer)
bar b@(Bar s) = (s, natVal b)

main :: IO ()
main = do
    i <- readLn
    let Just someNat = someNatVal i
    case someNat of
        SomeNat (_ :: Proxy n) -> do
            let a :: Bar (n + 5)
                a = Bar "as"
            print $ bar a

我得到的错误信息是

    Could not deduce (KnownNat (n + 5)) arising from a use of ‘bar’
    from the context (KnownNat n)
      bound by a pattern with constructor
                 SomeNat :: forall (n :: Nat). KnownNat n => Proxy n -> SomeNat,
               in a case alternative
      at Blag.hs:19:9-30
    In the second argument of ‘($)’, namely ‘bar a’
    In a stmt of a 'do' block: print $ bar a
    In the expression:
      do { let a :: Bar (n + 5)
               a = Bar "as";
           print $ bar a }
Failed, modules loaded: none.

为什么编译器不能推导出KnownNat (n + 5)来自 KnownNat n ?

Answer 1

第一个示例通过 someNatVal 的纯粹魔法起作用，制造类型级 Nat以及与之相关的知识。在第二个示例中，您知道 n ，但你问的是 n+5 .这行不通有两个原因。

第一个问题是类型系统会将所有“额外”实例视为不连贯的。也就是说，它需要知道 KnownNat 2和 KnownNat 7还有 KnownNat n => KnownNat (n + 5)和 KnownNat n => KnownNat (5 + n)等等。这些实例都会相互冲突，所以编译器需要关于如何处理这种情况的特殊内置知识，一切都会相当痛苦。

另一个问题是 TypeLits很单纯。它们似乎没有您期望从类型级自然中获得的有用归纳结构。

由于这些问题，似乎对于许多目的来说，简单高效TypeLit机制必须放在一边，以支持 The Slow Way，您可以在 singleton-nats 中找到手工构建的一元自然数。 .您需要单独的函数来处理值和类型级别的计算，但至少类型检查器将确保它们正确匹配，并且有一些 Template Haskell 将尝试使同时编写更容易。